Lecturer
Norbert Preining
JAIST, Research Center for Software Verification, Japan
Place/Time
WADT 2014: 22nd International Workshop on Algebraic Development Techniques
September 2014, Sinaia, Romania.
Abstract
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 
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.