Skip to Main content Skip to Navigation
Conference papers

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.
Complete list of metadata

https://hal.inria.fr/inria-00525132
Contributor : Ist Inria Nancy Grand Est Connect in order to contact the contributor
Submitted on : Monday, October 11, 2010 - 11:49:02 AM
Last modification on : Friday, September 21, 2018 - 8:02:04 PM

Identifiers

  • HAL Id : inria-00525132, version 1

Collections

Citation

Johannes Faber. Verification Architectures: Compositional Reasoning for Real-time Systems. Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.152-167. ⟨inria-00525132⟩

Share

Metrics

Record views

17