Specification Of Embedded, Real-time Systems

An approach to requirements specification and subsequent verification of designs for embedded, real-time systems is presented. A system is given by a conventional mathematical model for a dynamic system, where application specific state variables denote total finctions of real time. Specifications are formulas in a real-time, interval temporal logic, where atomic predicates define durations of states. Requirements are specified by a conjunction of formulas, which reflect safety and functionality constraints on the total system. A design specifies the behaviour of components and the conjunction of component specifications can be shown to imply the requirements. Designs can be refined in a similar fashion.