inria-00070674, version 1
Factorising temporal specifications
Marieke Huisman 1Kerry Trentelman
N° RR-5326 (2004)
Résumé : 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 specification language we use the so-called specification patterns, developed at SAnToS. 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.
- 1 : EVEREST (INRIA Sophia Antipolis)
- INRIA
- Domaine : Informatique/Autre
- Mots-clés : SPECIFICATION / PROGRAM VERIFICATION / JAVA / MULTI-THREADING / TEMPORAL LOGIC
- Référence interne : RR-5326
- inria-00070674, version 1
- http://hal.inria.fr/inria-00070674
- oai:hal.inria.fr:inria-00070674
- Contributeur : Rapport De Recherche Inria
- Soumis le : Vendredi 19 Mai 2006, 21:11:07
- Dernière modification le : Mercredi 31 Mai 2006, 14:24:25






Documents associés

Exporter