Projects per year
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.
Original language | English |
---|---|
Journal | International Journal on Software Tools for Technology Transfer |
Pages (from-to) | 1-29 |
Number of pages | 29 |
ISSN | 1433-2779 |
DOIs | |
Publication status | Published - Aug 2013 |
Keywords
- Real-time systems
- Stepwise-refinement
- Compositional verification
- Timed I/O automata
Fingerprint
Dive into the research topics of 'Real-time specifications'. Together they form a unique fingerprint.Projects
- 1 Finished
-
MT-Lab - Modelling of Information Technology
Wasowski, A. (CoI), Godskesen, J. C. (PI), Song, L. (CoI), Traonouez, L.-M. (CoI) & Biondi, F. (CoI)
01/11/2008 → 31/10/2013
Project: Research