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.
Number of pages | 21 |
---|
Publication status | Published - 1997 |
---|