Specifying and verifying requirements of real-time systems

Anders P. Ravn, Hans Rischel, Kirsten Mark Hansen

    Research output: Contribution to journalJournal articleResearchpeer-review

    703 Downloads (Pure)

    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 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
    Original languageEnglish
    JournalI E E E Transactions on Software Engineering
    Volume19
    Issue number1
    Pages (from-to)41-55
    ISSN0098-5589
    DOIs
    Publication statusPublished - 1993

    Bibliographical note

    Copyright: 1993 IEEE. Personal use of this material is permitted. However, permission to reprint/republish this material for advertising or promotional purposes or for creating new collective works for resale or redistribution to servers or lists, or to reuse any copyrighted component of this work in other works must be obtained from the IEEE

    Cite this