Specifying and verifying requirements of real-time systems

Abstract

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 state variables denote total functions of real time. Specifications are formulas in a real-time interval logic, where predicates define durations of states. Requirements are specified by a conjunction of formulas, which reflect safety and functionality constraints on the system. A system design includes specifications for sensor, rtctuator and program components. Programs have state variables which traces the history of communicated messages, while a sensor or actuator relate a trace with system states. A design is specified by a conjunction of component specifications. Verification is a proof that design implies requirements.