
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
A.P. Atlee, H. Gannon, "Specifying and Verifying Requirements of RealTime Systems," IEEE Transactions on Software Engineering, vol. 19, no. 1, pp. 4155, January, 1993.  
BibTex  x  
@article{ 10.1109/32.210306, author = {A.P. Atlee and H. Gannon}, title = {Specifying and Verifying Requirements of RealTime Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {19}, number = {1}, issn = {00985589}, year = {1993}, pages = {4155}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.210306}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Specifying and Verifying Requirements of RealTime Systems IS  1 SN  00985589 SP41 EP55 EPD  4155 A1  A.P. Atlee, A1  H. Gannon, PY  1993 KW  realtime systems; specification of requirements; verification of design; mathematical model; duration calculus; realtime interval logic; toplevel design; control law; sensor; actuator; distributed computation; synchronous events; formal specification; formal verification; realtime systems; temporal logic VL  19 JA  IEEE Transactions on Software Engineering ER   
An approach to specification of requirements and verification of design for realtime 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 realtime interval logic, where predicates define durations of states. Requirements define safety and functionality constraints on the system or a component. A toplevel 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 toplevel 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. 124154, 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. 210211.
[5] J. Dawes,The VDMSL 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. 12351246, 1990.
[7] R. C. Dorf,Modern Control Systems, AddisonWesley Series in Electrical Engineering, 3rd ed. Reading, MA: AddisonWesley, 1980.
[8] C. Ghezzi, D. Mandrioli, and A. Morzenti, "TRIO: A logic language for executable specifications of realtime systems,"J. Systems Software, vol. 12, pp. 107123, 1990.
[9] A. Goswami, M. Bell, and M. Joseph, "ISL: An interval logic for the specification of realtime programs," inProc. 2. Int. Symp. Formal Techniques in RealTime and FaultTolerant Systems, J. Vytopil, Ed.,LNCS571. New York: SpringerVerlag, 1991, pp. 120.
[10] R. Hale, "Temporal logic programming," inTemporal Logic and Their Applications, A. Galton, Ed. New York: Academic, 1987, pp. 91119.
[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. SE6, 1, pp. 213, 1980.
[13] K. M. Hansen, A. P. Ravn, and H. Rischel, "Specifying and verifying requirements of realtime systems," inProc. ACM SIGSOFT '91 Conf. On Software for Critical Systems, New Orleans, LA, Dec. 46, 1991;ACM Software Engineering Notes, vol. 15, no. 5, pp. 4454, 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. 231274, 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: SpringerVerlag, 1989.
[18] M. S. Jaffe, N. G. Leveson, M. P. E. Heimdahl, and B. E. Melhart, "Software requirements analysis for realtime processcontrol systems,"IEEE Trans. Software Eng., vol. SE17, no. 3, pp. 241258, 1991.
[19] F. Jahanian and A. K. Mok, "Safety analysis of timing properties in realtime systems,"IEEE Trans. Software Eng., vol. SE12, no. 9, pp. 890904, Sept. 1986.
[20] He Jifeng and J. Bowen, "Time interval semantics of a realtime programming Language, inProc. 4th Euromicro Workshop on RealTime Systems, Athens, Greece, June 35, 1992, pp. 110115.
[21] R. Koymans, "Specifying realtime properties with metric temporal logic,"RealTime Systems, vol. 2, no. 4, pp. 255299, 1990.
[22] L. Ljung,System Identification. Theory for the User. Englewood Cliffs, NJ: PrenticeHall, 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 realtime software,"IEEE Trans. Software Eng., vol. 14, no. 10, pp. 14091423, 1988.
[25] K. Marzullo, "Tolerating failures of continuousvalued sensors," Tech. Rep. TR901156, Dept. of Computer Science, Cornell University, Ithaca, NY, Sept. 1990.
[26] O. Maler, Z. Manna, and A. Pnueli, "From timed to hybrid systems," inProc. RealTime: Theory in Practice, REX Workshop, Mook, The Netherlands, June 1991, LNCS 600, 1992, pp. 447484.
[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 0055, 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 0056, 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. C18, 2, pp. 1019, 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. 6177.
[32] D. L. Parnas and P. C. Clements, "A rational design process: How and why to fake it,"IEEE Trans. Software Eng., vol. SE12, pp. 251257, Feb. 1986.
[33] D. L. Parnas, G. J. K. Asmis, and J. Madey, "Assessment of safetycritical software," Tech. Rep. 90295, 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 realtime systems," inProc. Formal Techniques in RealTime and FaultTolerant Systems (LNCS 331), pp. 8498, 1988.
[36] A. P. Ravn, H. Rischel, and V. Stavridou, "Provably correct safety critical software," inProc. IFAC SAFECOMP'90, London, England, Oct. 1990, pp. 1329.
[37] A. P. Ravn and H. Rischel, "Requirements capture for embedded realtime Systems, inProc. IMACSMCTS'91 Symp. Modeling and Control of Technological Systems, vol. 2, Villeneuve d'Ascq, France, 1991, pp. 147152.
[38] G. M. Reed and A. W. Roscoe, "Metric spaces as models for realtime 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 safetycritical systems: A train set example," inProc. 21st Symp. on FaultTolerant Computing, 1991, pp. 478485.
[40] F. B. Schneider, "The state machine approach: A tutorial,"Computing Surveys, vol. 22, no. 3, 1990.
[41] S. Schneider, "Correctness and communication of realtime systems," Ph.D. dissertation, 1989, Tech. Monograph PRG84, Oxford Univ. Computer Laboratory, England, March 1990.
[42] R. L. Schwartz, P. M. MelliarSmith, and F. H. Vogt, "An interval logic for higherlevel temporal reasoning," inProc. 2nd Annual ACM Symp. on Principles of Distributed Computing, 1983, pp. 173186.
[43] A. C. Shaw, "Reasoning about time inhigherlevel language software,"IEEE Trans. Software Eng., vol. 15, no. 7, pp. 875889, 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. 259294, 1991.
[47] Z. Chaochen, C. A. R. Hoare, and A. P. Ravn, "A calculus of durations,"Information Processing Lett., vol. 40, no. 5, pp. 269276, 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 RealTime and FaultTolerant Systems, LNCS 571, J. Vytopil, Ed., 1991, pp. 2132.