Automatic Verification of Parametric Specifications with Complex Topologies

Abstract : The focus of this paper is on reducing the complexity in verification by exploiting modularity at various levels: in specification, in verification, and structurally. For specifications, we use the modular language CSP-OZ-DC, which allows us to decouple verification tasks concerning data from those concerning durations. At the verification level, we exploit modularity in theorem proving for rich data structures and use this for invariant checking. At the structural level, we analyze possibilities for modular verification of systems consisting of various components which interact.We illustrate these ideas by automatically verifying safety properties of a case study from the European Train Control System standard, which extends previous examples by comprising a complex track topology with lists of track segments and trains with different routes.
Type de document :
Communication dans un congrès
Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

Littérature citée [26 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00523033
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : jeudi 7 octobre 2010 - 17:32:07
Dernière modification le : samedi 18 août 2018 - 14:34:01
Document(s) archivé(s) le : lundi 10 janvier 2011 - 11:09:05

Fichiers

ifm10-faber-ihlemann-jacobs-so...
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00523033, version 1
  • ARXIV : 1010.1602

Collections

Citation

Johannes Faber, Carsten Ihlemann, Swen Jacobs, Viorica Sofronie-Stokkermans. Automatic Verification of Parametric Specifications with Complex Topologies. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 2010, Lecture Notes in Computer Science. 〈inria-00523033〉

Partager

Métriques

Consultations de la notice

102

Téléchargements de fichiers

162