
This Article  
 
Share  
Bibliographic References  
Add to:  
Digg Furl Spurl Blink Simpy Del.icio.us Y!MyWeb  
Search  
 
ASCII Text  x  
Rajeev Alur, Thomas A. Henzinger, PeiHsin Ho, "Automatic Symbolic Verification of Embedded Systems," IEEE Transactions on Software Engineering, vol. 22, no. 3, pp. 181201, March, 1996.  
BibTex  x  
@article{ 10.1109/32.489079, author = {Rajeev Alur and Thomas A. Henzinger and PeiHsin Ho}, title = {Automatic Symbolic Verification of Embedded Systems}, journal ={IEEE Transactions on Software Engineering}, volume = {22}, number = {3}, issn = {00985589}, year = {1996}, pages = {181201}, doi = {http://doi.ieeecomputersociety.org/10.1109/32.489079}, publisher = {IEEE Computer Society}, address = {Los Alamitos, CA, USA}, }  
RefWorks Procite/RefMan/Endnote  x  
TY  JOUR JO  IEEE Transactions on Software Engineering TI  Automatic Symbolic Verification of Embedded Systems IS  3 SN  00985589 SP181 EP201 EPD  181201 A1  Rajeev Alur, A1  Thomas A. Henzinger, A1  PeiHsin Ho, PY  1996 KW  Specification and verification KW  realtime and hybrid systems KW  model checking KW  symbolic analysis KW  temporal logic. VL  22 JA  IEEE Transactions on Software Engineering ER   
Abstract—We present a modelchecking procedure and its implementation for the automatic verification of embedded systems. The system components are described as
[1] R. Alur, C. Courcoubetis, and D. Dill, "ModelChecking in Dense RealTime," Information and Computation, pp. 234, 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. 334, 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. 183235, 1994.
[5] R. Alur, T. Feder, and T. Henzinger, "The Benefits of Relaxing Punctuality," Proc. 10th ACM Symp. Principles of Distributed Computing, pp. 139152, 1991.
[6] R. Alur and T.A. Henzinger, "A Really Temporal Logic," J. ACM, vol. 41, no. 1, pp. 181204, 1994.
[7] R. Alur, T.A. Henzinger, and M.Y. Vardi, "Parametric RealTime Reasoning," Proc. 25th Ann. Symp. Theory of Computing, pp. 592601. ACM Press, 1993.
[8] Hybrid Systems III R. Alur, T.A. Henzinger, and E. Sontag, eds., Lecture Notes in Computer Science. SpringerVerlag, 1996.
[9] Hybrid Systems II, P. Antsaklis, A. Nerode, W. Kohn, and S. Sastry, eds., Lecture Notes in Computer Science, vol. 999. SpringerVerlag, 1995.
[10] A. Bouajjani, R. Echahed, and J. Sifakis, "On Model Checking for RealTime Properties with Durations," Proc. Eighth Ann. Symp. Logic in Computer Science, pp. 147159. 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.: SpringerVerlag, May 1981.
[12] E.M. Clarke, E.A. Emerson, and A.P. Sistla, "Automatic verification of finitestate concurrent systems using temporal logic specifications," ACM Trans. Programming Languages and Systems, vol. 8, no. 2, pp. 244263, 1986.
[13] Z. Chaochen, C.A.R. Hoare, and A.P. Ravn, "A Calculus of Durations," Information Processing Letters, vol. 40, pp. 269276, 1991.
[14] J.C. Corbett, "Modeling and Analysis of RealTime Ada Tasking Programs," K. Ramamritham, ed., Proc. RealTime Systems Symp., IEEE CS Press, pp. 132141, Dec. 1994.
[15] D.L. Dill, "Timing Assumptions and Verification of FiniteState Concurrent Systems," CAV 89: Automatic Verification Methods for Finitestate Systems, J. Sifakis, ed., Lecture Notes in Computer Science, vol. 407, pp. 197212. SpringerVerlag, 1989.
[16] C. Daws and S. Yovine, "Two Examples of Verification of Multirate Timed Automata Using Kronos," Proc. 16th Ann. Realtime Systems Symp., pp. 6675. IEEE CS Press, 1995.
[17] J. Ferrante and C. Rackoff, "A Decision Procedure for the FirstOrder Theory of Real Addition with Order," SIAM J. Computing, vol. 4, no. 1, pp. 6976, 1975.
[18] Hybrid Systems, R.L. Grossman, A. Nerode, A.P. Ravn, and H. Rischel, eds., Lecture Notes in Computer Science, vol. 736. SpringerVerlag, 1993.
[19] N. Halbwachs, "Delay Analysis in Synchronous Programs," CAV 93: Computeraided Verification, C. Courcoubetis, ed., Lecture Notes in Computer Science, vol. 697, pp. 333346. SpringerVerlag, 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. 324335. SpringerVerlag, 1995.
[21] T.A. Henzinger and P.H. Ho, "Algorithmic Analysis of Nonlinear Hybrid Systems," CAV 95: Computeraided Verification, P. Wolper, ed., Lecture Notes in Computer Science, vol. 939, pp. 225238. SpringerVerlag, 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: SpringerVerlag, 1995.
[23] T.A. Henzinger and P.H. Ho., "A Note on AbstractInterpretation 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. 252264. SpringerVerlag, 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. 453462,Milwaukee, Wisconsin, IEEE, Oct. 1995.
[25] T.A. Henzinger, P.H. Ho, and H. WongToi, "HyTech: The Next Generation," Proc. RealTime Systems Symp., IEEE CS Press, 1995.
[26] T.A. Henzinger, P.H. Ho, and H. WongToi, "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. 4171. SpringerVerlag, 1995. Full version available as Technical Report CSDTR951532, 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. 373382. ACM Press, 1995.
[28] T.A. Henzinger, X. Nicollin, J. Sifakis, and S. Yovine, "Symbolic Model Checking for RealTime 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. 223237. SpringerVerlag, 1994.
[31] P.H. Ho and H. WongToi, "Automated Analysis of an Audio Control Protocol," CAV 95: Computeraided Verification, P. Wolper, ed., Lecture Notes in Computer Science, vol. 939, pp. 381394. SpringerVerlag, 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. 179208. SpringerVerlag, 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 FiniteState Concurrent Programs Satisfy their Linear Specification," Proc. 12th Ann. Symp. Principles of Programming Languages, pp. 97107. ACM Press, 1985.
[35] K.G. Larsen, P. Petterson, and W. Yi, “Compositional and Symbolic ModelChecking of RealTime Systems,” Proc. 16th IEEE RealTime Systems Symp., pp. 7687, 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. 447484. SpringerVerlag, 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. 149178. SpringerVerlag, 1993.
[39] X. Nicollin, J. Sifakis, and S. Yovine, "From ATP to Timed Graphs and Hybrid Systems," Acta Informatica, vol. 30, pp. 181202, 1993.
[40] J.P. Queille and J. Sifakis, "Specification and Verification of Concurrent Systems in CESAR," Int'l Symp. Programming, pp. 337351, Lecture Notes in Computer Science 137, SpringerVerlag, Apr. 1982.
[41] S. Wolfram, Mathematica: A System for Doing Mathematics by Computer.New York: AddisonWesley, 1988.
[42] H. WongToi, "Symbolic Approximations for Verifying RealTime 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. WongToi, "Linear PhasePortrait Approximations for Nonlinear Hybrid Systems," in [8].