This Article 
 Bibliographic References 
 Add to: 
Specifying and Verifying Requirements of Real-Time Systems
January 1993 (vol. 19 no. 1)
pp. 41-55

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.

[1] J.F. Allen, "Maintaining Knowledge About Temporal Intervals,"Comm. ACM, Vol. 26, No. 11, Nov. 1983, pp. 832- 843.
[2] J. F. Allen, "Towards a general theory of action and time,"Artificial Intell., vol. 23, no. 2, pp. 124-154, July 1984.
[3] D. Bjørner, "A ProCoS project description," ESPRIT BRA 3104,EATCS Bull., no. 39, Oct. 1989.
[4] A. Davis and P. Freeman, "Requirements Engineering,"IEEE Trans. Software Eng., Mar. 1991, pp. 210-211.
[5] J. Dawes,The VDM-SL reference guide. Pitmann, 1991.
[6] M. Degl'Innocenti, G. L. Ferrari, G. Pacini, and F. Turini, "RSF: A formalism for executable requirement specifications,"IEEE Trans. Software Eng., vol. 16, no. 11, pp. 1235-1246, 1990.
[7] R. C. Dorf,Modern Control Systems, Addison-Wesley Series in Electrical Engineering, 3rd ed. Reading, MA: Addison-Wesley, 1980.
[8] C. Ghezzi, D. Mandrioli, and A. Morzenti, "TRIO: A logic language for executable specifications of real-time systems,"J. Systems Software, vol. 12, pp. 107-123, 1990.
[9] A. Goswami, M. Bell, and M. Joseph, "ISL: An interval logic for the specification of real-time programs," inProc. 2. Int. Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, J. Vytopil, Ed.,LNCS571. New York: Springer-Verlag, 1991, pp. 1-20.
[10] R. Hale, "Temporal logic programming," inTemporal Logic and Their Applications, A. Galton, Ed. New York: Academic, 1987, pp. 91-119.
[11] A. G. Hamilton,Logic for Mathematicians, rev. ed. New York: Cambridge University Press, 1988.
[12] K. L. Heninger, "Specifying software Rrequirements for complex systems: New techniques and their application,IEEE Trans. Software Eng., vol. SE-6, 1, pp. 2-13, 1980.
[13] K. M. Hansen, A. P. Ravn, and H. Rischel, "Specifying and verifying requirements of real-time systems," inProc. ACM SIGSOFT '91 Conf. On Software for Critical Systems, New Orleans, LA, Dec. 4-6, 1991;ACM Software Engineering Notes, vol. 15, no. 5, pp. 44-54, 1991.
[14] C. C. Zhou and M. R. Hansen, "Semantics and completeness of duration calculus," ProCoS Working Paper, accepted for the REX'92 Symp.
[15] D. Harel, "Statecharts: A visual formalism for complex systems,"Sci. Comput. Program., vol. 8, pp. 231-274, 1987.
[16] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[17] A. Isidori,Nonlinear Control Systems, Communications and Control Engineering Series. New York: Springer-Verlag, 1989.
[18] M. S. Jaffe, N. G. Leveson, M. P. E. Heimdahl, and B. E. Melhart, "Software requirements analysis for real-time process-control systems,"IEEE Trans. Software Eng., vol. SE-17, no. 3, pp. 241-258, 1991.
[19] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in real-time systems,"IEEE Trans. Software Eng., vol. SE-12, no. 9, pp. 890-904, Sept. 1986.
[20] He Jifeng and J. Bowen, "Time interval semantics of a real-time programming Language, inProc. 4th Euromicro Workshop on Real-Time Systems, Athens, Greece, June 3-5, 1992, pp. 110-115.
[21] R. Koymans, "Specifying real-time properties with metric temporal logic,"Real-Time Systems, vol. 2, no. 4, pp. 255-299, 1990.
[22] L. Ljung,System Identification. Theory for the User. Englewood Cliffs, NJ: Prentice-Hall, 1987.
[23] D. G. Luenberger,Introduction to Dynamic Systems. Theory, Models&Applications. New York: Wiley, 1979.
[24] Luqui, V. Berzins, and R. T. Yeh, "A prototyping language for real-time software,"IEEE Trans. Software Eng., vol. 14, no. 10, pp. 1409-1423, 1988.
[25] K. Marzullo, "Tolerating failures of continuous-valued sensors," Tech. Rep. TR90-1156, Dept. of Computer Science, Cornell University, Ithaca, NY, Sept. 1990.
[26] O. Maler, Z. Manna, and A. Pnueli, "From timed to hybrid systems," inProc. Real-Time: Theory in Practice, REX Workshop, Mook, The Netherlands, June 1991, LNCS 600, 1992, pp. 447-484.
[27] "The procurement of safety critical software in defence equipment; Part 1: Requirements, The procurement of safety critical software in defence equipment; Part 2: Guidance," Tech. Rep. INT DEF STAN 00-55, Ministry of Defence, Directorate of Standardization, Glasgow, Scotland, Apr. 1991.
[28] "Hazard analysis and safety classification of the computer and programmable electronic system elements of defence equipment," Tech. Rep. INT DEF STAN 00-56, Ministry of Defence, Directorate of Standardization, Glasgow, Scotland, Apr. 1991.
[29] B. Moszkowski, "A temporal logic for multilevel reasoning about hardware,"IEEE Trans. Comput., vol. C-18, 2, pp. 10-19, 1985.
[30] X. Nicollin, J. Sifakis, and S. Yovine, "From atp to timed graphs and hybrid systems," Draft Tech. Rep., June 1991.
[31] E.-R. Olderog, "Toward a design calculus for communicating programs,"Concur '91, 2nd International Conference on Concurrency Theory, Amsterdam, The Netherlands, Aug. 1991,LNCS527, 1991, pp. 61-77.
[32] D. L. Parnas and P. C. Clements, "A rational design process: How and why to fake it,"IEEE Trans. Software Eng., vol. SE-12, pp. 251-257, Feb. 1986.
[33] D. L. Parnas, G. J. K. Asmis, and J. Madey, "Assessment of safetycritical software," Tech. Rep. 90-295, TRIO, Queen's University, Kingston, Ontario, Canada, Dec. 1990.
[34] D. L. Parnas and J. Madey, "Functional documentation for computer system engineering" (version 2), CSL Rep. 237, TRIO, McMaster University, Hamilton, Ontario, Canada, Sept. 1991.
[35] A. Pnueli and E. Harel, "Applications of temporal logic to the specification of real-time systems," inProc. Formal Techniques in Real-Time and Fault-Tolerant Systems (LNCS 331), pp. 84-98, 1988.
[36] A. P. Ravn, H. Rischel, and V. Stavridou, "Provably correct safety critical software," inProc. IFAC SAFECOMP'90, London, England, Oct. 1990, pp. 13-29.
[37] A. P. Ravn and H. Rischel, "Requirements capture for embedded real-time Systems, inProc. IMACS-MCTS'91 Symp. Modeling and Control of Technological Systems, vol. 2, Villeneuve d'Ascq, France, 1991, pp. 147-152.
[38] G. M. Reed and A. W. Roscoe, "Metric spaces as models for real-time concurrency," inProc. Math. Found. of Computer Science, LNCS 298, 1987.
[39] A. Saeed, R. de Lemos, and T. Anderson, "The role of formal methods in the requirements analysis of safety-critical systems: A train set example," inProc. 21st Symp. on Fault-Tolerant Computing, 1991, pp. 478-485.
[40] F. B. Schneider, "The state machine approach: A tutorial,"Computing Surveys, vol. 22, no. 3, 1990.
[41] S. Schneider, "Correctness and communication of real-time systems," Ph.D. dissertation, 1989, Tech. Monograph PRG-84, Oxford Univ. Computer Laboratory, England, March 1990.
[42] R. L. Schwartz, P. M. Melliar-Smith, and F. H. Vogt, "An interval logic for higher-level temporal reasoning," inProc. 2nd Annual ACM Symp. on Principles of Distributed Computing, 1983, pp. 173-186.
[43] A. C. Shaw, "Reasoning about time in-higher-level language software,"IEEE Trans. Software Eng., vol. 15, no. 7, pp. 875-889, 1989.
[44] J. M. Spivey,The Z Notation: A Reference Manual (Computer Science Series). Englewood Cliffs, NJ: Prentice Hall International, 1989.
[45] E. V. Sørensen, A. P. Ravn, and H. Rischel, "Control program for a gas burner: Part 1: Informal requirements, ProCoS case study 1," ProCoS Rep. ID/DTH EVS2, 1990.
[46] J. C. Willems, "Paradigms and puzzles in the theory of dynamical systems,"IEEE Trans. Automat. Contr., vol. 36, no. 3, pp. 259-294, 1991.
[47] Z. Chaochen, C. A. R. Hoare, and A. P. Ravn, "A calculus of durations,"Information Processing Lett., vol. 40, no. 5, pp. 269-276, 1991.
[48] Z. Chaochen, M. R. Hansen, A. P. Ravn, and H. Rischel, "Duration specifications for shared processors," inProc. 2nd Int. Symp. on Formal Techniques in Real-Time and Fault-Tolerant Systems, LNCS 571, J. Vytopil, Ed., 1991, pp. 21-32.

Index Terms:
real-time systems; specification of requirements; verification of design; mathematical model; duration calculus; real-time interval logic; top-level design; control law; sensor; actuator; distributed computation; synchronous events; formal specification; formal verification; real-time systems; temporal logic
A.P. Atlee, H. Gannon, "Specifying and Verifying Requirements of Real-Time Systems," IEEE Transactions on Software Engineering, vol. 19, no. 1, pp. 41-55, Jan. 1993, doi:10.1109/32.210306
Usage of this product signifies your acceptance of the Terms of Use.