Verifying Liveness Properties in Isabelle/HOL

Description

Background

With the growth in complexity of algorithms and designs, the importance of formal verification - proving or disproving a set of correctness properties underlying a system - has been raised. Formal verification of correctness properties becomes even more paramount when concurrent and distributed systems are considered. Correctness properties are usually partitioned into safety properties - something bad will not occur - and liveness - something good will eventually happen.

While the verification of safety properties is theoretically well established and ready to be deployed at large scale (e.g. [GHE15]), the ensurance of liveness properties is far less understood though it is as crucial as safety when it comes to the analysis of distributed systems. Researchers from the Australian National University (ANU) and from Data61, CSIRO have formulated an assumption called justness that is claimed to be exactly right for proving a large class of liveness properties [vGH19]. The idea behind justness is that independent parallel components should not block each other from executing enabled actions. Since justness seems to always hold in real-life implementations, it is considered as a warranted replacement of classical fairness assumptions.

Research Questions and Tasks

To promote justness as the fundamental assumption for verifying liveness properties and to provide a scale-able verification framework, the following two problems need to be addressed.

  • When verifying liveness properties of a large system, computer scientists often transform the system into a smaller one that behaves semantically equivalent with respect to the properties at hand. To prove that liveness properties are preserved under this transformation, semantic equivalences are used. Unfortunately, classical semantic equivalences, such as bisimilarity, between systems do not accord well with justness [vGH19]. To overcome this deficiency, we currently develop several new semantic equivalences by augmenting each transition of a labelled transition system with the names of the (concurrent) components that are required for that transition.
  • For each and every equivalence we prove fundamental properties, such as preservation of justness. As the proofs are often very similar, proof mechanization provides an undeniable advantage: no slip of pen, no oversight, no typos. Moreover, replaying existing proofs in newly developed equivalences speeds up proof development, as it indicates those proof steps that are no longer valid -- one can thus concentrate on important changes in the proof.

To support our research, the internship aims at the development of a proof theory in the proof assistant Isabelle/HOL [NPW02] for justness-preserving semantic equivalences."requirements: "knowledge of the proof assistant Isabelle/HOL is an advantage, but not a prerequisite; however knowledge in (computational) logic and discrete mathematics is required

References

[GHE15]
P. Gammie, A.L. Hosking & K.Engelhardt (2015): Relaxing Safely: Verified On-the-fly Garbage Collection for x86-TSO. In D. Grove & S. Blackburn, editors: Programming Language Design and Implementation (PLDI'15), ACM, pp. 99-109, doi: 10.1145/2737924.2738006.
[vGH19]
R.J. van Glabbeek & P. Höfner (2019): Progress, Justness, and Fairness. ACM Computing Surveys 52(4), pp. 69:1-69:38, doi: 10.1145/3329125.
[NPW02]
T. Nipkow, L.C. Paulson & M. Wenzel (2002): Isabelle/HOL — A Proof Assistant for Higher-OrderLogic. Lecture Notes in Computer Science 2283, Springer, doi: 10.1007/3-540-45949-9.

Keywords

formal methods, logic, interactive theorem proving, verification

Updated:  1 June 2019/Responsible Officer:  Head of School/Page Contact:  CECS Marketing