Conferences in Research and Practice in Information Technology
  

Online Version - Last Updated - 20 Jan 2012

 

 
Home
 

 
Procedures and Resources for Authors

 
Information and Resources for Volume Editors
 

 
Orders and Subscriptions
 

 
Published Articles

 
Upcoming Volumes
 

 
Contact Us
 

 
Useful External Links
 

 
CRPIT Site Search
 
    

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
 

 

ACS Logo© Copyright Australian Computer Society Inc. 2001-2014.
Comments should be sent to the webmaster at crpit@scem.uws.edu.au.
This page last updated 16 Nov 2007