Specifying and verifying requirements of real-time systems

Anders P. Ravn, Hans Rischel, Kirsten Mark Hansen

    Research output: Contribution to journalJournal articleResearchpeer-review

    617 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

    Ravn, Anders P. ; Rischel, Hans ; Hansen, Kirsten Mark. / Specifying and verifying requirements of real-time systems. In: I E E E Transactions on Software Engineering. 1993 ; Vol. 19, No. 1. pp. 41-55.
    @article{233519fbfbc34666aff1631f0ecbb5fa,
    title = "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 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",
    author = "Ravn, {Anders P.} and Hans Rischel and Hansen, {Kirsten Mark}",
    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",
    year = "1993",
    doi = "10.1109/32.210306",
    language = "English",
    volume = "19",
    pages = "41--55",
    journal = "I E E E Transactions on Software Engineering",
    issn = "0098-5589",
    publisher = "Institute of Electrical and Electronics Engineers",
    number = "1",

    }

    Specifying and verifying requirements of real-time systems. / Ravn, Anders P.; Rischel, Hans; Hansen, Kirsten Mark.

    In: I E E E Transactions on Software Engineering, Vol. 19, No. 1, 1993, p. 41-55.

    Research output: Contribution to journalJournal articleResearchpeer-review

    TY - JOUR

    T1 - Specifying and verifying requirements of real-time systems

    AU - Ravn, Anders P.

    AU - Rischel, Hans

    AU - Hansen, Kirsten Mark

    N1 - 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

    PY - 1993

    Y1 - 1993

    N2 - 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

    AB - 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

    U2 - 10.1109/32.210306

    DO - 10.1109/32.210306

    M3 - Journal article

    VL - 19

    SP - 41

    EP - 55

    JO - I E E E Transactions on Software Engineering

    JF - I E E E Transactions on Software Engineering

    SN - 0098-5589

    IS - 1

    ER -