Verification Architectures: Compositional Reasoning for Real-time Systems

Abstract : We introduce a conceptual approach to decompose real-time systems, specified by integrated formalisms: instead of showing safety of a system directly, one proves that it is an instance of a Verification Architecture, a safe behavioural protocol with unknowns and local realtime assumptions. We examine how different verification techniques can be combined in a uniform framework to reason about protocols, assumptions, and instantiations of protocols. The protocols are specified in CSP, extended by data and unknown processes with local assumptions in a real-time logic. To prove desired properties, the CSP dialect is embedded into dynamic logic and a sequent calculus is presented. Further, we analyse the instantiation of protocols by combined specifications, here illustrated by CSP-OZ-DC. Using an example, we show that this approach helps us verify specifications that are too complex for direct verification.
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, 6396, pp.152-167, 2010, Lecture Notes in Computer Science
Liste complète des métadonnées

https://hal.inria.fr/inria-00525132
Contributeur : Ist Inria Nancy Grand Est <>
Soumis le : lundi 11 octobre 2010 - 11:49:02
Dernière modification le : lundi 11 octobre 2010 - 11:49:02

Identifiants

  • HAL Id : inria-00525132, version 1

Collections

Citation

Johannes Faber. Verification Architectures: Compositional Reasoning for Real-time Systems. Mery, Dominique and Merz, Stephan. Integrated Formal Methods - IFM 2010, Oct 2010, Nancy, France. Springer Berlin / Heidelberg, 6396, pp.152-167, 2010, Lecture Notes in Computer Science. 〈inria-00525132〉

Partager

Métriques

Consultations de la notice

12