Verifying duration properties of timed transition systems

Zhiming Liu, Anders P. Ravn, Xiaoshan Li

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


    This paper proposes a method for formal real-time systems development:Requirements and high level design decisions are time interval properties and are therefore specified in the Duration Calculus (DC), while implementations are described bytimed transition systems (TTS). A link from implementation properties tothe requirement and design properties is given by interpreting a DC formula in a model of the executions of a TTS andthen providing rules for lifting properties proved by structuralinduction for a TTS to DC formulas. The method is illustrated by the Gas Burner case study.
    Original languageEnglish
    Title of host publicationProceedings of the IFIP Working Conference on Programming Concepts and Methods
    PublisherChapman & Hall
    Publication date1998
    Publication statusPublished - 1998
    EventPROCOMET'98 -
    Duration: 1 Jan 1998 → …


    Period01/01/1998 → …

    Cite this