Analyzing the dynamics of a Z specification.
In: Calmet, J and Limongelli, C, (eds.)
We present a method for analyzing the dynamics of a Z document describing a non-sequential system. First a formal operational semantics based on the chemical metaphor is given to Z. Then, some Unity-like temporal logic constructs are defined on such a formal operational semantics in order to allow the specification and analysis of dynamic and temporal properties of concurrent systems, such as safety and liveness properties.
|Title:||Analyzing the dynamics of a Z specification|
|UCL classification:||UCL > School of BEAMS > Faculty of Engineering Science
UCL > School of BEAMS > Faculty of Engineering Science > Computer Science
Archive Staff Only