This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Automatic Symbolic Verification of Embedded Systems
March 1996 (vol. 22 no. 3)
pp. 181-201

Abstract—We present a model-checking procedure and its implementation for the automatic verification of embedded systems. The system components are described as Hybrid Automata—communicating machines with finite control and real-valued variables that represent continuous environment parameters such as time, pressure, and temperature. The system requirements are specified in a temporal logic with stop watches, and verified by symbolic fixpoint computation. The verification procedure—implemented in the Cornell Hybrid Technology Tool, HYTECH—applies to hybrid automata whose continuous dynamics is governed by linear constraints on the variables and their derivatives. We illustrate the method and the tool by checking safety, liveness, time-bounded, and duration requirements of digital controllers, schedulers, and distributed algorithms.

[1] R. Alur, C. Courcoubetis, and D. Dill, "Model-Checking in Dense Real-Time," Information and Computation, pp. 2-34, vol. 104, 1993.
[2] R. Alur, C. Courcoubetis, N. Halbwachs, T. Henzinger, P. Ho, X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "The Algorithmic Analysis of Hybrid Systems," Theoretical Computer Science, vol. 138, pp. 3-34, 1995.
[3] R. Alur, C. Courcoubetis, T.A. Henzinger, and P.-H. Ho, Hybrid Automata: An Algorithmic Approach to the Specification and Verification of Hybrid Systems Hybrid Systems, R.L. Grossman, A. Nerode, A. Ravn, and H. Rischel, eds., 1993.
[4] R. Alur and D. Dill, “A Theory of Timed Automata,” Theoretical Computer Science, vol. 126, pp. 183-235, 1994.
[5] R. Alur, T. Feder, and T. Henzinger, "The Benefits of Relaxing Punctuality," Proc. 10th ACM Symp. Principles of Distributed Computing, pp. 139-152, 1991.
[6] R. Alur and T.A. Henzinger, "A Really Temporal Logic," J. ACM, vol. 41, no. 1, pp. 181-204, 1994.
[7] R. Alur, T.A. Henzinger, and M.Y. Vardi, "Parametric Real-Time Reasoning," Proc. 25th Ann. Symp. Theory of Computing, pp. 592-601. ACM Press, 1993.
[8] Hybrid Systems III R. Alur, T.A. Henzinger, and E. Sontag, eds., Lecture Notes in Computer Science. Springer-Verlag, 1996.
[9] Hybrid Systems II, P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, eds., Lecture Notes in Computer Science, vol. 999. Springer-Verlag, 1995.
[10] A. Bouajjani, R. Echahed, and J. Sifakis, "On Model Checking for Real-Time Properties with Durations," Proc. Eighth Ann. Symp. Logic in Computer Science, pp. 147-159. IEEE CS Press, 1993.
[11] E.M. Clarke and E.A. Emerson, "Synthesis of synchronization skeletons for branching time temporal logic," Logic of Programs: Workshop, Lecture notes in Computer Science. vol. 131. Yorktown Heights, N. Y.: Springer-Verlag, May 1981.
[12] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finite-state concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244-263, 1986.
[13] Z. Chaochen, C.A.R. Hoare, and A.P. Ravn, "A Calculus of Durations," Information Processing Letters, vol. 40, pp. 269-276, 1991.
[14] J.C. Corbett, "Modeling and Analysis of Real-Time Ada Tasking Programs," K. Ramamritham, ed., Proc. Real-Time Systems Symp., IEEE CS Press, pp. 132-141, Dec. 1994.
[15] D.L. Dill, "Timing Assumptions and Verification of Finite-State Concurrent Systems," CAV 89: Automatic Verification Methods for Finite-state Systems, J. Sifakis, ed., Lecture Notes in Computer Science, vol. 407, pp. 197-212. Springer-Verlag, 1989.
[16] C. Daws and S. Yovine, "Two Examples of Verification of Multirate Timed Automata Using Kronos," Proc. 16th Ann. Real-time Systems Symp., pp. 66-75. IEEE CS Press, 1995.
[17] J. Ferrante and C. Rackoff, "A Decision Procedure for the First-Order Theory of Real Addition with Order," SIAM J. Computing, vol. 4, no. 1, pp. 69-76, 1975.
[18] Hybrid Systems, R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, eds., Lecture Notes in Computer Science, vol. 736. Springer-Verlag, 1993.
[19] N. Halbwachs, "Delay Analysis in Synchronous Programs," CAV 93: Computer-aided Verification, C. Courcoubetis, ed., Lecture Notes in Computer Science, vol. 697, pp. 333-346. Springer-Verlag, 1993.
[20] T.A. Henzinger, "Hybrid Automata with Finite Bisimulations," ICALP 95: Automata, Languages, and Programming, Z. Fülöp and F. Gécseg, eds., Lecture Notes in Computer Science, vol. 944, pp. 324-335. Springer-Verlag, 1995.
[21] T.A. Henzinger and P.-H. Ho, "Algorithmic Analysis of Nonlinear Hybrid Systems," CAV 95: Computer-aided Verification, P. Wolper, ed., Lecture Notes in Computer Science, vol. 939, pp. 225-238. Springer-Verlag, 1995.
[22] T. Henzinger and P.-H. Ho, "HyTech: The Cornell Hybrid Technology Tool," Proc. 1994 Workshop on Hybrid Systems and Autonomous Control, Lecture Notes in Computer Science. New York: Springer-Verlag, 1995.
[23] T.A. Henzinger and P.-H. Ho., "A Note on Abstract-Interpretation Strategies for Hybrid Automata," Hybrid Systems II, P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, eds., Lecture Notes in Computer Science, vol. 999, pp. 252-264. Springer-Verlag, 1995.
[24] M.R. Henzinger, T.A. Henzinger, and P.W. Kopke, "Computing Simulations on Finite and Infinite Graphs," Proc.: 36th Ann. Symp. Foundations of Computer Science, pp. 453-462,Milwaukee, Wisconsin, IEEE, Oct. 1995.
[25] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "HyTech: The Next Generation," Proc. Real-Time Systems Symp., IEEE CS Press, 1995.
[26] T.A. Henzinger, P.-H. Ho, and H. Wong-Toi, "A User Guide to HYTECH," TACAS 95: Tools and Algorithms for the Construction and Analysis of Systems, E. Brinksma, W.R. Cleaveland, K.G. Larsen, T. Margaria, and B. Steffen, eds., Lecture Notes in Computer Science, vol. 1,019, pp. 41-71. Springer-Verlag, 1995. Full version available as Technical Report CSD-TR-95-1532, Cornell Univ.
[27] T.A. Henzinger, P.W. Kopke, A. Puri, and P. Varaiya, "What's Decidable about Hybrid Automata?" Proc. 27th Ann. Symp. Theory of Computing, pp. 373-382. ACM Press, 1995.
[28] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, "Symbolic Model Checking for Real-Time Systems," Information and Computation, vol. 111, no. 2, 1994.
[29] P.-H. Ho, "Automatic Analysis of Hybrid Systems," PhD thesis, Cornell Univ., 1995.
[30] N. Halbwachs, P. Raymond, and Y.-E. Proy, "Verification of Linear Hybrid Systems by Means of Convex Approximation," SAS 94: Static Analysis Symp., B. LeCharlier, ed., Lecture Notes in Computer Science, vol. 864, pp. 223-237. Springer-Verlag, 1994.
[31] P.-H. Ho and H. Wong-Toi, "Automated Analysis of an Audio Control Protocol," CAV 95: Computer-aided Verification, P. Wolper, ed., Lecture Notes in Computer Science, vol. 939, pp. 381-394. Springer-Verlag, 1995.
[32] Y. Kesten, A. Pnueli, J. Sifakis, and S. Yovine, "Integration Graphs: A Class of Decidable Hybrid Systems," Hybrid Systems, R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, eds., Lecture Notes in Computer Science, vol. 736, pp. 179-208. Springer-Verlag, 1993.
[33] L. Lamport, “A Fast Mutual Exclusion Algorithm,” ACM Trans. Computer Systems, vol. 5, no. 1, pp. 1–11, 1987.
[34] O. Lichtenstein and A. Pnueli, "Checking that Finite-State Concurrent Programs Satisfy their Linear Specification," Proc. 12th Ann. Symp. Principles of Programming Languages, pp. 97-107. ACM Press, 1985.
[35] K.G. Larsen, P. Petterson, and W. Yi, “Compositional and Symbolic Model-Checking of Real-Time Systems,” Proc. 16th IEEE Real-Time Systems Symp., pp. 76-87, Dec. 1995.
[36] K.L. McMillan, Symbolic Model Checking. Kluwer Academic, 1993.
[37] O. Maler, Z. Manna, and A. Pnueli, "From Timed to Hybrid Systems," Real Time: Theory in Practice, J.W. de Bakker, K. Huizing, W.-P. de Roever, and G. Rozenberg, eds., Lecture Notes in Computer Science, vol. 600, pp. 447-484. Springer-Verlag, 1992.
[38] X. Nicollin, A. Olivero, J. Sifakis, and S. Yovine, "An Approach to the Description and Analysis of Hybrid Systems," Hybrid Systems, R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, eds., Lecture Notes in Computer Science, vol. 736, pp. 149-178. Springer-Verlag, 1993.
[39] X. Nicollin, J. Sifakis, and S. Yovine, "From ATP to Timed Graphs and Hybrid Systems," Acta Informatica, vol. 30, pp. 181-202, 1993.
[40] J.-P. Queille and J. Sifakis, "Specification and Verification of Concurrent Systems in CESAR," Int'l Symp. Programming, pp. 337-351, Lecture Notes in Computer Science 137, Springer-Verlag, Apr. 1982.
[41] S. Wolfram, Mathematica: A System for Doing Mathematics by Computer.New York: Addison-Wesley, 1988.
[42] H. Wong-Toi, "Symbolic Approximations for Verifying Real-Time Systems," PhD thesis, Stanford Univ., 1994.
[43] R. Alur and R.P. Kurshan, "Timing Analysis with COSPAN," in [8].
[44] T.A. Henzinger and H. Wong-Toi, "Linear Phase-Portrait Approximations for Nonlinear Hybrid Systems," in [8].

Index Terms:
Specification and verification, real-time and hybrid systems, model checking, symbolic analysis, temporal logic.
Citation:
Rajeev Alur, Thomas A. Henzinger, Pei-Hsin Ho, "Automatic Symbolic Verification of Embedded Systems," IEEE Transactions on Software Engineering, vol. 22, no. 3, pp. 181-201, March 1996, doi:10.1109/32.489079
Usage of this product signifies your acceptance of the Terms of Use.