Refining System Requirements to Program Specifications

Ernst-Ruediger Olderog, Anders P. Ravn, Jens Ulrik Skakkebæk

    Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review


    A coherent and mathematically well-founded approach to the design ofreal-time and hybrid systems is presented.It covers requirementsanalysis and specification, design of controlling automatasatisfying the requirements, and derivation ofoccam-like communicating programs from these automata.The generalized railroad crossing due to Heitmeyer and Lynchillustrates the approach.Requirements are analyzed within aconventional dynamic systems model of a plant, where states arefunctions of the reals, representing time. The requirements arespecified in an assumption-commitment style using Duration Calculus,a real-time interval logic. Controlling real-time automata arespecified in the same formalism by elementaryconstraints on the plant states for each control state or phase.The Duration Calculus is used to verify that the control design refinesthe requirements.The real-time automata map smoothly to component descriptions in asystems design language that uses timed trace assertions over statetransition events to constrain control flow.Components can under certain conditions be transformed tooccam-like communicating programs.
    Original languageEnglish
    Title of host publicationFormal Methods in Real-Time Systems
    Publication date1996
    Publication statusPublished - 1996

    Cite this