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.
|Title of host publication||Proceedings of the IFIP Working Conference on Programming Concepts and Methods|
|Publisher||Chapman & Hall|
|Publication status||Published - 1998|
|Event||PROCOMET'98 - |
Duration: 1 Jan 1998 → …
|Period||01/01/1998 → …|