Real-Time Specifications

David, Alexandre;Larsen Kim, Guldstrand;Legay, Axel;Nyman, Ulrik;Wasowski, Andrzej;et.al.
(2015) Software Tools for Technology Transfer (STTT) — Vol. 17, n° 1, p. 17-45 (2015)

Files

No attached file found for this publication.

Details

Authors
  • David, Alexandre
    Author
  • Larsen Kim, Guldstrand
    Author
  • Legay, AxelUCLouvain
    Author
  • Nyman, Ulrik
    Author
  • Wasowski, Andrzej
    Author
Show more
Abstract
A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation, and a set of operators supporting stepwise design. We develop a specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications -- all indispensable ingredients of a compositional design methodology.The theory is implemented in the new tool Ecdar. We present symbolic versions of the algorithms used in Ecdar, and demonstrate the use of the tool using a small case study in compositional verification.
Affiliations

Citations

  • APA
  • Chicago
  • FWB

David, A., Larsen Kim, G., Legay, A., Nyman, U., Traonouez, L.-M., & Wasowski, A. (2015). Real-Time Specifications. Software Tools for Technology Transfer (STTT), 17(1), 17-45. https://doi.org/10.1007/s10009-013-0286-x (Original work published 2015)