Duration Properties of Timed Transition Systems

Zhiming Liu, Anders P. Ravn, Xiaoshan Li

    Research output: Book/ReportReportResearchpeer-review


    This paper proposes a method for formal real-time systems development.The system requirements and high level design decisions are time interval properties, and are therefore specified in the Duration Calculus (DC), while the implementation and refinement are described in termsof timed 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 and then providing rules for lifting properties proved for a TTS to DC. The method is illustrated by the Gas Burner case study.
    Original languageEnglish
    Number of pages21
    Publication statusPublished - 1997

    Cite this