Factorising Temporal Specifications

Marieke Huisman, Kerry Trentelman

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

Abstract

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.
Original languageEnglish
Title of host publicationTheory of Computing 2005, Eleventh CATS 2005, Computing: The Australasian Theory Symposium, Newcastle, NSW, Australia, January/February 2005
EditorsMike D. Atkinson, Frank K. H. A. Dehne
PublisherAustralian Computer Society
Pages87-96
Number of pages10
Publication statusPublished - 2005
Externally publishedYes
EventComputing: the Australasian Theory Symposium, CATS 2005 - Newcastle, Australia
Duration: 29 Jan 20051 Feb 2005

Publication series

NameConferences in Research and Practice in Information Technology
Volume41

Conference

ConferenceComputing: the Australasian Theory Symposium, CATS 2005
Abbreviated titleCATS 2005
CountryAustralia
CityNewcastle
Period29/01/051/02/05

Fingerprint Dive into the research topics of 'Factorising Temporal Specifications'. Together they form a unique fingerprint.

Cite this