Journal article
Specifying and verifying requirements of real-time systems
An approach to specification of requirements and verification of design for real-time systems is presented. A system is defined by a conventional mathematical model for a dynamic system where application specific states denote functions of real time. Specifications are formulas in duration calculus, a real-time interval logic, where predicates define durations of states.
Requirements define safety and functionality constraints on the system or a component. A top-level design is given by a control law: a predicate that defines an automation controlling the transition between phases of operation. Each phase maintains certain relations among the system states; this is analogous to the control functions known from conventional control theory.
The top-level design is decomposed into an architecture for a distributed system with specifications for sensor, actuator, and program components. Programs control the distributed computation through synchronous events. Sensors and actuators relate events with system states. Verification is a deduction showing that a design implies requirements
Language: | English |
---|---|
Publisher: | IEEE |
Year: | 1993 |
Pages: | 41-55 |
ISSN: | 19393520 , 00985589 and 23263881 |
Types: | Journal article |
DOI: | 10.1109/32.210306 |
Actuators Automatic control Calculus Control systems Design automation Logic Mathematical model Real time systems Safety Sensor systems actuator control law distributed computation duration calculus formal specification formal verification mathematical model real-time interval logic real-time systems sensor specification of requirements synchronous events temporal logic top-level design verification of design