| 1 |
Verification Architectures: Compositional Reasoning for Real-time Systems
|
|
|
|
In: Integrated Formal Methods - IFM 2010 ; https://hal.inria.fr/inria-00525132 ; Integrated Formal Methods - IFM 2010, INRIA Nancy Grand Est, Oct 2010, Nancy, France. pp.152-167 (2010)
|
|
Abstract:
The original publication is available at www.springerlink.com. ; International audience ; 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.
|
|
Keyword:
[INFO.INFO-LO]Computer Science [cs]/Logic in Computer Science [cs.LO]; [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE]; ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.1: Requirements/Specifications; ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.2: Design Tools and Techniques; ACM: D.: Software/D.2: SOFTWARE ENGINEERING/D.2.4: Software/Program Verification; Compositional Verification; CSP; Duration Calculus; Object-Z; Real-Time System; Sequent calculus
|
|
URL: https://hal.inria.fr/inria-00525132
|
|
BASE
|
|
Hide details
|
|
|
|
|
