Proving liveness properties using abstract state machines and n-visibility


Norbert Preining
JAIST, Research Center for Software Verification, Japan


WADT 2014: 22nd International Workshop on Algebraic Development Techniques
September 2014, Sinaia, Romania.


One methodolgy for formal specification of a complex system is by using Abstract State Machine (Asm). Here states describe the actual state of the system, and transitions change the state. Although this is a very simple paradigm, it renders itself applicable in a wide variety of scenarios, from program analysis over protocol specification to design planning. In the setting of formal, more specifically algebraic specification and verification, we aim at giving a set of conditions, or properties, on the states, which we want to prove to hold in all reachable states.

In the following we will describe the general methodology in proving properties using Asm. In particular we will extend one of the most common proof methods, namely induction over the set of reachable states, to include additional properties on transitions. This new proof method, we call it n-visibility (for n \in  \mathbb{N} \cup \infty), allows for the specification and verification of liveness properties, which by itself are out of the reach of the base proof method by induction on the set of reachable states.

We then continue in defining an extended system that includes transitions, and show that the base proof method in the extended system and the proof method with n-visibility in the base system coincides. Using this method we can show that extension with infinite visibility acts as fix-point of this extension procedure, and can proof all properties that one can proof with ∞-visibility, including the typical liveness properties, but also more exotic fairness properties.

Leave a comment

Your email address will not be published. Required fields are marked *