s'authentifier
version française rss feed

inria-00070674, version 1

Factorising temporal specifications

Marieke Huisman 1, Kerry 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.

  • Domaine : Informatique/Autre
  • Mots-clés : SPECIFICATION / PROGRAM VERIFICATION / JAVA / MULTI-THREADING / TEMPORAL LOGIC
  • Référence interne : RR-5326
 
  • inria-00070674, version 1
  • oai:hal.inria.fr:inria-00070674
  • Contributeur : 
  • Soumis le : Vendredi 19 Mai 2006, 21:11:07
  • Dernière modification le : Mercredi 31 Mai 2006, 14:24:25
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...
tous les articles de la base du CCSd...