Abstract
We present a novel approach for verifying safety properties of finite state machines communicating over unbounded FIFO channels that is based on applying machine learning techniques. We assume that we are given a model of the system and learn the set of reachable states from a sample set of executions of the system, instead of attempting to iteratively compute the reachable states. The learnt set of reachable states is then used to either prove that the system is safe or to produce a valid execution of the system leading to an unsafe state (i.e. a counterexample). We have implemented this method for verifying FIFO automata in a tool called Lever that uses a regular language learning algorithm called RPNI. We apply our tool to a few case studies and report our experience with this method. We also demonstrate how this method can be generalized and applied to the verification of other infinite state systems.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Bouajjani, A., Jonsson, B., Nilsson, M., Touili, T.: Regular model checking. In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 403–418. Springer, Heidelberg (2000)
Oncina, J., Garcia, P.: Inferring regular languages in polynomial update time. In: Pattern Recognition and Image Analysis. Series in Machine Perception and Artificial Intelligence, vol. 1, pp. 49–61. World Scientific, Singapore (1992)
Dupont, P.: Incremental regular inference. In: Miclet, L., de la Higuera, C. (eds.) ICGI 1996. LNCS, vol. 1147, pp. 222–237. Springer, Heidelberg (1996)
Vardhan, A., Sen, K., Viswanathan, M., Agha, G.: Learning to verify safety properties, Tech. Rep. UIUCDCS-R-2004-2445 University of Illinois (2004), http://osl.cs.uiuc.edu/docs/sub2004vardhan/cfsmLearn.pdf
Hopcroft, J.E., Motwani, R., Rotwani, Ullman, J.D.: Introduction to Automata Theory, Languages and Computability. Addison-Wesley Longman Publishing Co. Inc., Amsterdam (2000)
Berstel, J.: Transductions and Context-Free-Languages. B.G. Teubner, Stuttgart (1979)
Angluin, D.: Learning regular sets from queries and counterexamples. Inform. Comput. 75(2), 87–106 (1987)
Gold, E.M.: Language indentification in the limit. Inform. Control 10, 447–474 (1967)
Finkel, A., Purushothaman Iyer, S., Sutre, G.: Well-abstracted transition systems: Application to FIFO automata. Information and Computation 181(1), 1–31 (2003)
LEVER, Learning to verify tool (2004), http://osl.cs.uiuc.edu/vardhan/lever.html
Møller, A.: http://www.brics.dk/~amoeller/automaton/ (2004)
Tanenbaum, A.S.: Computer Networks, 2nd edn. Prentice-Hall, Englewood Cliffs (1989)
Nilsson, M.: http://www.regulalrmodelchecking.com (2004)
Abdulla, P.A., Jonsson, B., Nilsson, M., d’Orso, J.: Algorithmic improvements in regular model checking. In: Hunt Jr., W.A., Somenzi, F. (eds.) CAV 2003. LNCS, vol. 2725, pp. 236–248. Springer, Heidelberg (2003)
Boigelot, B.: Symbolic Methods for Exploring Infinite State Spaces, Ph.D. thesis, Collection des Publications de la Faculté des Sciences Appliquées de l’Université de Liége (1999)
Bouajjani, A., Habermehl, P.: Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations. Theoretical Computer Science 221(1–2), 211–250 (1999)
Touili, T.: Regular model checking using widening techniques. In: ENTCS, vol. 50, Elsevier, Amsterdam (2001)
Bultan, T.: Automated symbolic analysis of reactive systems, Ph.D. thesis, Dept. of Computer Science, University of Maryland, College Park, Md. (1998)
Bartzis, C., Bultan, T.: Widening arithmetic automata. In: Computer Aided Verification 2004 (to appear, 2004)
Peled, D., Vardi, M.Y., Yannakakis, M.: Black box checking. In: FORTE/PSTV, Beijing, China (1999)
Groce, A., Peled, D., Yannakakis, M.: Adaptive model checking. In: Katoen, J.-P., Stevens, P. (eds.) TACAS 2002. LNCS, vol. 2280, pp. 357–371. Springer, Heidelberg (2002)
Cobleigh, J.M., Giannakopoulou, D., Pasareanu, C.S.: Learning assumptions for compositional verification. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 331–346. Springer, Heidelberg (2003)
Boigelot, B., Godefroid, P.: Automatic synthesis of specifications from the dynamic observation of reactive programs. In: Brinksma, E. (ed.) TACAS 1997. LNCS, vol. 1217, pp. 321–334. Springer, Heidelberg (1997)
Ammons, G., Bodík, R., Larus, J.R.: Mining specifications. ACM SIGPLAN Notices 37(1), 4–16 (2002)
Edelkamp, S., Lafuente, A., Leue, S.: Protocol verification with heuristic search. In: AAAI Symposium on Model-based Validation of Intelligence (2001)
Ernst, M.D., Cockrell, J., Griswold, W.G., Notkin, D.: Dynamically discovering likely program invariants to support program evolution. In: International Conference on Software Engineering (ICSE 1999), pp. 213–224 (1999)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Vardhan, A., Sen, K., Viswanathan, M., Agha, G. (2004). Learning to Verify Safety Properties. In: Davies, J., Schulte, W., Barnett, M. (eds) Formal Methods and Software Engineering. ICFEM 2004. Lecture Notes in Computer Science, vol 3308. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-30482-1_26
Download citation
DOI: https://doi.org/10.1007/978-3-540-30482-1_26
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-23841-6
Online ISBN: 978-3-540-30482-1
eBook Packages: Springer Book Archive