Factorising Temporal Specifications

Huisman, M. and Trentelman, K.

    This paper proposes a method to factorise the verification of temporal properties for multi-threaded programs over groups of different threads. Essentially, the method boils down to showing that there exists a group of threads that establishes the property of interest, while the remaining threads do not affect it. We fine-tune the method by identifying for each property particular conditions under which the preservation is necessary. As a specification language we use the so-called specification patterns developed as part of the Bandera project at Kansas State University. For each specification pattern we propose a decomposition rule. We have shown the soundness of each rule using the pattern mappings as defined for LTL. The proofs have been formalised using the theorem prover Isabelle.
Cite as: Huisman, M. and Trentelman, K. (2005). Factorising Temporal Specifications. In Proc. Eleventh Computing: The Australasian Theory Symposium (CATS2005), Newcastle, Australia. CRPIT, 41. Atkinson, M. and Dehne, F., Eds. ACS. 87-96.
pdf (from crpit.com) pdf (local if available) BibTeX EndNote GS