Real-time specifications

Alexandre David, Kim Guldstrand Larsen, Axel Legay, Ulrik Mathias Nyman, Louis-Marie Traonouez, Andrzej Wasowski

    Research output: Journal Article or Conference Article in JournalJournal articleResearchpeer-review

    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 languageEnglish
    JournalInternational Journal on Software Tools for Technology Transfer
    Pages (from-to)1-29
    Number of pages29
    ISSN1433-2779
    DOIs
    Publication statusPublished - 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.

    Cite this