This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Guest A Layered Approach to Automating the Verification of Real-Time Systems
September 1992 (vol. 18 no. 9)
pp. 768-784

A layered approach to the specification and verification of real-time systems is described. Application processes are specified in the CSR Application Language, which includes high-level language constructs such as timeouts, deadlines, periodic processes, interrupts, and exception handling. A configuration schema is used to map the processes to system resources, and to specify the communication links between them. The authors automatically translate the result of the mapping into the CCSR process algebra, which characterizes CSR's resource-based computation model by a prioritized transition system. For the purposes of verification, a reachability analyzer based on the CCSR semantics has been implemented. This tool mechanically evaluates the correctness of the CSR specification by checking whether an exception state can be reached in its corresponding CCSR term. The effectiveness of this technique is illustrated by a multisensor robot example.

[1] R. Alur and T. Henzinger, "Real-time logics: Complexity and expressiveness," inProc. IEEE Symp. Logic in Computer Science, 1990.
[2] A. Bernstein and P. K. Harter Jr., "Proving real-time properties of programs with temporal logic," inProc. Symp. Operating Systems Principles, 1981.
[3] S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe, "A theory of communicating sequential processes,"J. ACM, vol. 31, no. 3, pp. 560-599, July 1984.
[4] R. Backhouse, P. Chisholm, G. Malcolm, and E. Saaman, "Do-it-yourself type theory,"Formal Aspects Computing, vol. 1, pp. 19- 84, 1989.
[5] R. Gerber, "Communicating shared resources: A model for distributed real-time systems," Ph.D. dissertation, Department of Computer and Information Science, University of Pennsylvania, 1991.
[6] R. Gerber, E. Gunter, and I. Lee, "Implementing a real-time process algebra in HOL," inProc. IEEE Int. Workshop on the HOL Theorem Proving System, IEEE Press, Aug. 1991.
[7] R. Gerber and I. Lee, "A proof system for communicating shared resources," inProc. 11th IEEE Real-Time Systems Symp., 1990.
[8] R. Gerth and A. Boucher, "A timed failure semantics for extended communicating processes," inProc. ICALP '87, LNCS 267, 1987.
[9] C. Ghezzi and R. Kemmerer, "ASTRAL: An assertional language for specifying realtime systems,"Tech. Rep. TRCS 90-25, Department of Computer Science, University of California, Santa Barbara, 1990.
[10] 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.
[11] D. Harel, "Statecharts: A visual formalism for complex systems,"Sci. Comput. Program., vol. 8, pp. 231-274, 1987.
[12] E. Harel, O. Lichtenstein, and A. Pnueli, "Explicit clock temporal logic," inProc. IEEE Symp. Logic in Computer Science, 1990.
[13] R. Harper, "Introduction to standard ML,"Tech. Rep. ECS-LFCS-86-14, Department of Computer Science, University of Edinburgh, Scotland, 1986.
[14] T. A. Henziger, Z. Manna, and A. Pnueli, "Temporal proof methodologies for real-time systems," inProc. 18th ACM Symp. Principles of Programming Languages, pp. 353-366, 1991.
[15] C.A.R. Hoare,Communicating Sequential Processes, Prentice Hall, Englewood, N.J., 1985.
[16] 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.
[17] F. Jahanian and D. A. Stuart, "A method for verifying properties of modechart specifications," inProc. IEEE Real-Time Systems Symp., pp. 12-21, Dec. 1988.
[18] M. Joseph and A. Goswami, "What's 'real' about real-time systems?" inIEEE Real-Time Systems Symp., 1988.
[19] R. Koymans, "Specifying message passing and time-critical systems with temporal logic,"Real-Time Systems, vol. 16, Nov. 1990.
[20] I. Lee and V. Gehlot, "Language constructs for distributed real-time programming," inProc. IEEE Real-Time Systems Symp., 1985.
[21] R. Milner, "Calculi for synchrony and asynchrony.Theoretical Computer Science, vol. 25, pp. 267-310, 1983.
[22] R. Milner,Communication and Concurrency, Englewood Cliffs, NJ: Prentice-Hall, 1989.
[23] J. S. Ostroff and W. M. Wonham, "Modeling, specifying and verifying real-time embedded computer systems," inProc. IEEE Real-Time Systems Symp., pp. 124-132, Dec. 1987.
[24] G. Plotkin, "A structural approach to operational semantics," Tech. Rep. DAIMI FN-19, Computer Science Dept., Aarhus University, 1981.
[25] 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.
[26] G. M. Reed and A. W. Roscoe, "Metric spaces as models for real-time concurrency," inProc. Math. Found. of Computer Science, LNCS 298, 1987.
[27] W. Yi, "CCS + Time = An interleaving model for real time systems," inProc. Int. Conf. Automata, Languages and Programming, 1991.
[28] A. Zwarico, "Timed acceptance: An algebra of time dependent computing," Ph.D. dissertation, Department of Computer and Information Science, University of Pennsylvania, 1988.

Index Terms:
layered approach; specification; verification; real-time systems; CSR Application Language; high-level language constructs; timeouts; deadlines; periodic processes; interrupts; exception handling; configuration schema; system resources; communication links; CCSR process algebra; resource-based computation model; prioritized transition system; reachability analyzer; CCSR semantics; correctness; exception state; multisensor robot example; calculus of communicating systems; exception handling; formal specification; formal verification; high level languages; real-time systems
Citation:
R. Gerber, I. Lee, "Guest A Layered Approach to Automating the Verification of Real-Time Systems," IEEE Transactions on Software Engineering, vol. 18, no. 9, pp. 768-784, Sept. 1992, doi:10.1109/32.159838
Usage of this product signifies your acceptance of the Terms of Use.