Verifying Temporal Properties of Reactive Systems by Transformation
arXiv:1512.03860 · doi:10.4204/EPTCS.199.3
Abstract
We show how program transformation techniques can be used for the verification of both safety and liveness properties of reactive systems. In particular, we show how the program transformation technique distillation can be used to transform reactive systems specified in a functional language into a simplified form that can subsequently be analysed to verify temporal properties of the systems. Example systems which are intended to model mutual exclusion are analysed using these techniques with respect to both safety (mutual exclusion) and liveness (non-starvation), with the errors they contain being correctly identified.
In Proceedings VPT 2015, arXiv:1512.02215. This work was supported, in part, by Science Foundation Ireland grant 10/CE/I1855 to Lero - the Irish Software Engineering Research Centre (www.lero.ie), and by the School of Computing, Dublin City University
Cited by in corpus (6)
- Verification of Programs via Intermediate Interpretation
- Finite Countermodel Based Verification for Program Transformation (A Case Study)
- Generating Counterexamples for Model Checking by Transformation
- Program Specialization as a Tool for Solving Word Equations
- On Solving Word Equations via Program Transformation
- Supercompiling String Programs Using Word Equations as Constraints