Validation of Automation Systems using Temporal Logic Model Checking and Groebner Bases

Authors: Quoc-Nam Tran, Anjib Mulepati

Abstract:

Validation of an automation system is an important issue. The goal is to check if the system under investigation, modeled by a Petri net, never enters the undesired states. Usually, tools dedicated to Petri nets such as DESIGN/CPN are used to make reachability analysis. The biggest problem with this approach is that it is impossible to generate the full occurence graph of the system because it is too large. In this paper, we show how computational methods such as temporal logic model checking and Groebner bases can be used to verify the correctness of the design of an automation system. We report our experimental results with two automation systems: the Automated Guided Vehicle (AGV) system and the traffic light system. Validation of these two systems ranged from 10 to 30 seconds on a PC depending on the optimizing parameters.

Keywords: Computational Intelligence, Temporal Logic Reasoning, Model Checking, Groebner Bases.

Digital Object Identifier (DOI): doi.org/10.5281/zenodo.1058389

References:

[1] A. Biere, A. Cimatti, E. M. Clarke, M. Fujita, andY. Zhu. Symbolic model checking using SAT proceduresinstead of BDDs. In Proceedings of Design AutomationConference (DAC99), 1999.
[2] A. Biere, A. Cimatti, E. M. Clarke, and Y. Zhu. Symbolicmodel checking without bdds. In Proceedings of TACAS,volume 1579 of LNCS. Springer, 1999.
[3] A. Biere, E. M. Clarke, R. Raimi, and Y. Zhu. Verifiyingsafety properties of a power pc microprocessor usingsymbolic model checking without bdds. In N. Halbwachsand D. Peled, editors, Proceedings of the 11th Inter-national Conference on Computer Aided Verification,CAV99, volume 1633 of LNCS, pages 6071, Trento,Italy, 1999.
[4] P. Bjesse, T. Leonard, and A. Mokkedem. Finding bugsin an alpha microprocessor using satisfiability solvers.In Proceedings of the 13th International Conference onComputer Aided Verification, CAV 2001, number 2102 inLNCS, pages 454464, Paris, France, 2001. Springer.
[5] B. Buchberger. An Algorithm for Finding a Basis for theResidue Class Ring of a Zero-dimensional PolynomialIdeal (in German). PhD thesis, Institute of Mathematics,Univ. Innsbruck, Innsbruck, Austria, 1965.
[6] B. Buchberger. An algorithmic criterion for the solvabil-ity of algebraic systems of equations (german). Aequa-tiones Mathematicae, 4:374383, 1970.
[7] B. Buchberger. Groebner Bases: An algorithmic methodin polynomial ideal theory. In N. K. Bose, editor,Multidimensional Systems Theory, chapter 6, pages 184232. Reidel Publishing Company, Dodrecht, 1985.
[8] O. Caprotti, A. Ferscha, and H. Hong. eachability testin petri nets by groebner bases. Technical report, RISC-Linz, 1995.
[9] E. Clarke and E. Emerson. Design and synthesis of syn-cronization of skeletons using branching time temporallogic. In Proceedings of the IBM workshop on logics ofprograms, volume 131 of LNCS, pages 5271. Springer,1981.
[10] E. Clarke, O. Grumberg, and D. Peled. Model Checking.The MIT Press, 1999.
[11] E. M. Clarke, O. Grumberg, and D. E. Long. Modelchecking and abstraction. ACM Transactions on Pro-gramming Languages and Systems, 16(5):15121542,1994.
[12] E. M. Clarke, D. E. Long, and K. L. McMillan. Com-positional model checking. In Proceedings of the FourthAnnual Symposium on Logic in computer science. IEEEPress, 1989.
[13] F. Copty, L. Fix, R. Fraer, E. Giunchiglia, G. Kamhi,A. Tacchella, and M. Y. Vardi. Benefits of boundedmodel checking at an industrial setting. In Proceedingsof the 13th International Conference on Computer AidedVerification, CAV 2001, number 2102 in LNCS, pages454464, Paris, France, 2001. Springer.
[14] P. Cousot. Abstract interpretation. ACM ComputingSurveys, 28(2):324328, 1996.
[15] D. Dams, R. Gerth, and O. Grumberg. Abstract in-terpretation of reactive systems. ACM Transaction onProgramming Languages and Systems, 19(2):253291,1997.
[16] E. A. Emerson and A. P. Sistla. Symmetry and modelchecking. Formal Methods in System Design, 1996.
[17] P. Godefroid and P. Wolper. Using partial orders forthe efficient verification of deadlock freedom and safetyproperties. Formal Methods in System Design, 1993.
[18] S. Graf and H. Sadi. Construction of abstract stategraphs with pvs. In Proceedings of CAV, volume 1254of LNCS, pages 7283. Springer, 1997.
[19] O. Grumberg and D. E. Long. Model checking and mod-ular verification. ACM Transactions on ProgrammingLanguages and Systems, 16(3):843871, 1994.
[20] V. Gyuris and A. P. Sistla. On-the-fly model checkingunder fairness that exploits symmetry. Formal Methodsin System Design, 15(3):217238, 1999.
[21] K. Heljanko. Combining Symbolic and Partial OrderMethods for Model Checking 1-Safe Petri Nets. PhD the-sis, Department of Computer Science and Engineering,Helsinki University of Technology, February 2002.
[22] C. N. Ip and D. L. Dill. Better verification throughsymmetry. Formal Methods in System Design, 9(1/2):4176, 1996.
[23] J.R. Burch, E.M. Clarke, K.L. McMillan, D.L. Dill, andL.J. Hwang. Symbolic Model Checking: 1020 Statesand Beyond. In Proceedings of the Fifth Annual IEEESymposium on Logic in Computer Science, pages 133,Washington, D.C., 1990. IEEE Computer Society Press.
[24] T. Junttila. On the symmetry reduction method for Petrinets and similar formalisms. PhD thesis, Laboratoryfor Theoretical Computer Science, Helsinki Universityof Technology, 2003.
[25] R. Kaivola. Equivalences, preorders and compositionalverification for linear time temporal logic and concurrentsystems. PhD thesis, Department of Computer Science,University of Helsinki, 1996.
[26] S. Katz and D. Peled. Verification of distributed programsusing representative interleaving sequences. DistributedComputing, 6(2):107120, 1992.
[27] B. H. Krogh and L. E. Holloway. Synthesis of feedbackcontrol logic for discrete manufacturing systems. Auto-matica, 27(4):641651, 1991.
[28] O. Kupferman and M. Vardi. From complementationto certification. In Proceedings of the 10th InternationalConference on Tools and Algorithms for the Constructionand Analysis of Systems, volume 2988 of LNCS, pages591606. Springer, 2004.
[29] O. Kupferman, M. Vardi, and P. Wolper. An automata-theoretic approach to branching-time model checking.Journal of the ACM, 47(2):312360, 2000.
[30] R. P. Kurshan. Computer Aided Verification of Coor-dinating Processes: The Automata-Theoretic Approach.Princeton University Press, 1994.
[31] K. L. McMillan. Symbolic Model Checking. KluwerAcademic Publishers, 1993.
[32] K. Namjoshi. Certifying model checker. In Proceed-ings of the 13th International Conference on Computer-Aided Verification, volume 2102 of LNCS, pages 213.Springer, 2001.
[33] D. Peled and L. Zuck. From model checking to atemporal proof. In Proceedings of the 8th InternationalSPIN Workshop, volume 2057 of LNCS, pages 114,Toronto, Canada, 2001. Springer.
[34] J. Peterson. Petri Net Theory and the Modeling ofSystems. Prentice Hall, 1981.
[35] L. Petrucci. Design and validation of a controller.In Proceedings of the 4th World Multiconference onSystemics, Cybernetics and Informatics (SCI), volume 8,2000.
[36] A. Pnueli. The temporal logic of programs. In Pro-ceedings of 18th IEEE Symposium on Foundation ofComputer Science, pages 4657, 1977.
[37] J. Quille and J. Sifakis. Specification and verification ofconcurrent systems in cesar. In Proceedings of the 5thInternational Symposium on Programming, page 1981,337350.
[38] K. Schmidt. How to calculate symmetries of petri nets.Acta Informatica, 36(7):545590, 2000.
[39] Q.-N. Tran. A fast algorithm for Groebner basis conver-sion and its applications. Journal of Symbolic Computa-tion, 30:451468, 2000.
[40] Q.-N. Tran. Efficient algorithms for implicitization usinggroebner walk. Journal of Computer Aided GeometricDesign, 21:837857, 2004.
[41] Q.-N. Tran. A new class of term orders for eliminationand applications. Journal of Symbolic Computation, 42,2007.
[42] Q.-N. Tran. A p-space algorithm for groebner basescomputation in boolean rings. In Proceedings of WorldAcademy of Science, Engineering and Technology, vol-ume 35, pages 495501, Paris, France, 2008.
[43] A. Valmari. A stubborn attack on state explosion. FormalMethods in System Design, 1(4):297322, 1992.
[44] A. Valmari. The state explosion problem. In W. Reisigand G. Rozenberg, editors, Lectures on Petri Nets I: BasicModels, Advances in Petri Nets, volume 1491 of LNCS,pages 429528. Springer, 1998.
[45] M. Vardi. Alternating automata and program verifica-tion. In Computer Science Today - Recent Trends andDevelopments, volume 1000 of LNCS, pages 471485.Springer-Verlag, 1995.
[46] M. Vardi. Automated verification = graphs, logic, andautomata. In Proceedings of IJCAI, 2003.
[47] M. Vardi and P. Wolper. Automata-theoretic techniquesfor modal logics of programs. Journal of Computer andSystem Science, 32(2):182221, 1986.
[48] M. Y. Vardi. An automata-theoretic approach to lineartemporal logic. In Logics for Concurrency: Structureversus Automata, volume 1043 of LNCS, pages 238266.Springer, 1996.
[49] M. Y. Vardi and P. Wolper. Reasoning about infinitecomputations. Information and Computation, 115(1):137, 1994.
[50] K. Varpaaniemi. On stubborn sets in the verificationof linear time temporal properties. Formal Methods inSystem Design, 26(1):4567, 2005.