Refining System Requirements to Program Specifications

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.