Subscribe

Issue No.02 - Feb. (2013 vol.39)

pp: 216-236

Stefan Leue , University of Konstanz, Konstanz

Wei Wei , SAP AG, Darmstadt

DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2011.1

ABSTRACT

Asynchronous reactive systems form the basis of a wide range of software systems, for instance in the telecommunications domain. It is highly desirable to rigorously show that these systems are correctly designed. However, traditional formal approaches to the verification of these systems are often difficult because asynchronous reactive systems usually possess extremely large or even infinite state spaces. We propose an integer linear program (ILP) solving-based property checking framework that concentrates on the local analysis of the cyclic behavior of each individual component of a system. We apply our framework to the checking of the buffer boundedness and livelock freedom properties, both of which are undecidable for asynchronous reactive systems with an infinite state space. We illustrate the application of the proposed checking methods to Promela, the input language of the SPIN model checker. While the precision of our framework remains an issue, we propose a counterexample guided abstraction refinement procedure based on the discovery of dependences among control flow cycles. We have implemented prototype tools with which we obtained promising experimental results on real-life system models.

INDEX TERMS

Unified modeling language, Complexity theory, Analytical models, Message passing, Integer linear programming, Mathematical model, Cost accounting, Promela, Software verification, formal methods, property checking, integer linear programming, static analysis, abstraction, refinement, counterexamples, asynchronous communication, buffer boundedness, livelock freedom, control flow cycles, cycle dependences, UML

CITATION

Stefan Leue, Wei Wei, "Integer Linear Programming-Based Property Checking for Asynchronous Reactive Systems",

*IEEE Transactions on Software Engineering*, vol.39, no. 2, pp. 216-236, Feb. 2013, doi:10.1109/TSE.2011.1REFERENCES

- [1] BEEM: Bemchmarks for Explicit Model Checkers, http://anna. fi.muni.cz/modelsindex.html , 2012.
- [2] Database of Promela Models, http://www.albertolluch.comindex.html. ?x=promelamodels.html , 2012.
- [3] A "Formal" Promela Model for CDMA-RLP Based on IS707-2, http://www.ferguson-by-bicycle.com/ sem_lit rlp-vp.htm, 2012.
- [4] lp_solve. http://tech.groups.yahoo.com/grouplp_solve /, 2012.
- [5] A Promela Model of Train Controllers, http://khorshid.ece.ut. ac. ir/rebeca/examples/ TrainControllertraincont roller.htm , 2012.
- [6] A Promela Model: Process Sleep and Wakeup on a Shared-Memory Multiprocessor, ftp://cm.bell-labs.com/cm/cs/who/gerardsleep_wakeup , 2012
- [7] The SPIN Website, http:/spinroot.com, 2012.
- [8] T. Ball, A. Podelski, and S.K. Rajamani, "Boolean and Cartesian Abstraction for Model Checking C Programs."
Int'l J. Software Tools for Technology Transfer, vol. 5, no. 1 pp. 49-58, 2003.- [9] M. Ben-Ari, "Principles of Concurrent and Distributed Programming," https://www.mcs.vuw.ac.nz/courses/COMP310 2007T2/, 2012.
- [10] W.R. Bevier, "Towards an Operational Semantics of PROMELA in ACL2,"
Proc. Third SPIN Workshop, 1997.- [11] A. Bouajjani and R. Mayr, "Model Checking Lossy Vector Addition Systems,"
Proc. 16th Ann. Symp. Theoretical Aspects of Computer Science vol. 1563, pp. 323-333, 1999.- [12] R.S. Boyer and J.S. Moore, "Program Verification,"
J. Automated Reasoning, vol. 1, no. 1 pp. 17-23, 1985.- [13] D. Brand and P. Zafiropulo, "On Communicating Finite-State Machines," Technical Report RZ 1053, IBM Zurich Research Lab, 1981
- [14] E.M. Clarke, O. Grumberg, S. Jha, Y. Lu, and H. Veith, "Counterexample-Guided Abstraction Refinement,"
Proc. 12th Int'l Conf. Computer Aided Verification, vol. 1855, pp. 154-169, 2000.- [15] E.M. Clarke, O. Grumberg, and D.A. Peled,
Model Checking. The MIT Press, 2000.- [16] S.A. Cook, "The Complexity of Theorem-Proving Procedures,"
Proc. Third Ann. ACM Symp. Theory of Computing, 1971.- [17] J.C. Corbett, "Automated Formal Analysis Methods for Concurrent and Real-Time Software," PhD thesis, Technical Report 92-48, Dept. of Computer Science, Univ. of Massachusetts at Amherst. 1992.
- [18] J.C. Corbett, "Evaluating Deadlock Detection Methods for Concurrent Software,"
IEEE Trans. Software Eng., vol. 22, no. 3, pp. 161-180, Mar. 1996.- [19] J.C. Corbett and G.S. Avrunin, "Using Integer Programming to Verify General Safety and Liveness Properties,"
Formal Methods in System Design, vol. 6, no. 1, pp. 97-123, 1995.- [20] T.H. Cormen, C.E. Leiserson, R.L. Rivest, and C. Stein,
Introduction to Algorithms, second ed. Columbia Univ., 2002.- [21] P. Cousot and R. Cousot, "Abstract Interpretation: A Unified Lattice Model for Static Analysis of Programs by Construction or Approximation of Fixpoints,"
Proc. Symp. Principles of Programming Languages, pp. 238-252, 1977.- [22] P. Cousot and N. Halbwachs, "Automatic Discovery of Linear Restraints among Variables of a Program,"
Proc. Fifth Ann. ACM Symp. Principles of Programming Languages, pp. 84-96, 1978.- [23] W. Damm and B. Jonsson, "Eliminating Queues from RT UML Model Representations,"
Proc. Seventh Int'l Symp. Formal Techniques in Real-Time and Fault-Tolerant Systems, vol. 2469, pp. 375-394, 2002.- [24] M. del Mar Gallardo, P. Merino, and E. Pimentel, "A Generalized Semantics of PROMELA for Abstract Model Checking,"
Formal Aspects of Computing, vol. 16, no. 3 pp. 166-193, 2004.- [25] Y. Dong, X. Du, G.J. Holzmann, and S.A. Smolka, "Fighting Livelock in the GNU i-Protocol: A Case Study in Explicit-State Model Checking,"
Int'l J. Software Tools for Technology Transfer, vol. 4, no. 4 pp. 505-528, 2003.- [26] J. Ellsberger, D. Hogrefe, and A. Sarma,
SDL: Formal Object-Oriented Language for Communicating Systems. Prentice-Hall, 1997.- [27] J. Esparza and S. Melzer, "Verification of Safety Properties using Integer Programming: Beyond the State Equation,"
Formal Methods in System Design, vol. 16, no. 2 pp. 159-189, 2000.- [28] J. Esparza and M. Nielsen, "Decidability Issues for Petri Nets—A Survey,"
Elektronische Informationsverarbeitung und Kybernetik, vol. 30, no. 3, pp. 143-160, 1994.- [29] A. Finkel, "A New Class of Analysable CFSMs with Unbounded FIFO Channels,"
Proc. Eighth IFIP WG6.1 Int'l Conf. Protocol Specification, Testing and Verification, 1988.- [30] A. Finkel and A. Choquet, "Simulation of Linear FIFO Nets by Petri Nets Having a Structured Set of Terminal Markings,"
Proc. Eighth Int'l Conf. Applications and Theory of Petri Nets, 1987.- [31] A. Finkel and L.E. Rosier, "A Survey on the Decidability Questions for Classes of FIFO Nets,"
Proc. Eighth European Workshop Applications and Theory of Petri Nets, vol. 340, pp. 106-132, 1987.- [32] A. Finkel and G. Vidal-Naquet,
Structuration des Systemes de Transitions-Applications au Controle du Parallelisme par Files FIFO, These Science, Paris 11, NewsletterInfo: 30. 1986.- [33] Formal Systems (Europe) Ltd.,
Failures-Divergences Refinement: FDR 2 User Manual, sixth ed., June 2005.- [34] M. Geilen and T. Basten, "Requirements on the Execution of Kahn Process Networks,"
Proc. 12th European Symp. Programming Languages and Systems, vol. 2618, pp. 319-334. 2003.- [35] M.G. Gouda, E.M. Gurari, T.-H. Lai, and L.E. Rosier, "On Deadlock Detection in Systems of Communicating Finite State Machines,"
Computers and Artificial Intelligence, vol. 6, no. 3, pp. 209-228, 1987.- [36] M.G. Gouda and L.E. Rosier, "On Deciding Progress for a Class of Communication Protocols,"
Proc. 18th Ann. Conf. Information Sciences and Systems, pp. 663-667, 1984.- [37] H. Hansen, W. Penczek, and A. Valmari, "Stuttering-Insensitive Automata for On-the-Fly Detection of Livelock Properties,"
Electronic Notes in Theoretical Computer Science, vol. 66, no. 2, pp. 178-193, 2002.- [38] G.J. Holzmann,
The Spin Model Checker: Primer and Reference Manual. Addison-Wesley, 2003.- [39] O.H. Ibarra, J. Su, Z. Dang, T. Bultan, and R.A. Kemmerer, "Counter Machines and Verification Problems."
Theoretical Computer Science, vol. 289, no. 1, pp. 165-189, 2002.- [40] C.N. Ip and D.L. Dill, "Better Verification through Symmetry,"
Formal Methods in System Design, vol. 9, nos. 1/2, pp. 41-75, 1996.- [41] T. Jéron and C. Jard, "Testing for Unboundedness of FIFO Channels,"
Theoretical Computer Science, vol. 113, no. 1, pp. 93-117, 1993.- [42] M. Kamel and S. Leue, "Formalization and Validation of the General Inter-ORB Protocol (GIOP) Using PROMELA and SPIN,"
Int'l J. Software Tools for Technology Transfer, vol. 2, no. 4, pp. 394-409, 2000.- [43] R.M. Karp and R.E. Miller, "Parallel Program Schemata,"
J. Computer and System Sciences, vol. 3, no. 2, pp. 147-195, 1969.- [44] L. Khachiyan, "A Polynomial Algorithm in Linear Programming,"
Doklady Akademii Nauk SSSR, vol. 244, pp. 1093-1096, 1979.- [45] S. Leue, A. Ştefănescu, and W. Wei, "A Livelock Freedom Analysis for Infinite State Asynchronous Reactive Systems,"
Proc. 17th Int'l Conf. Concurrency Theory, vol. 4137, pp. 79-94, 2006.- [46] S. Leue, R. Mayr, and W. Wei, "A Scalable Incomplete test for Message Buffer Overflow in Promela Models,"
Proc. 11th Int'l SPIN Workshop Model Checking Software, vol. 2989, pp. 216-233, 2004.- [47] S. Leue, R. Mayr, and W. Wei, "A Scalable Incomplete Test for the Boundedness of UML RT Models,"
Proc. 10th Int'l Conf. Tools and Algorithms for the Construction and Analysis of Systems, pp. 327-341, 2004.- [48] S. Leue, A. Stefanescu, and W. Wei, "Dependency Analysis for Control Flow Cycles in Reactive Communicating Processes,"
Proc. 15th Int'l SPIN Workshop Model Checking Software, vol. 5156, pp. 176-195, 2008.- [49] S. Leue and W. Wei, "Counterexample-Based Refinement for a Boundedness Test for CFSM Languages,"
Proc. 12th Int'l SPIN Workshop Model Checking Software, vol. 3639, pp. 58-74, 2005.- [50] R.J. Lipton, "The Reachability Problem Requires Exponential Space," Technical Report 62, Dept. of Computer Science, Yale Univ., 1976.
- [51] C. Liu, A. Kondratyev, Y. Watanabe, A.L. Sangiovanni-Vincentelli, and J. Desel, "Schedulability Analysis of Petri Nets Based on Structural Properties,"
Proc. Sixth Int'l Conf. Application of Concurrency to System Design, pp. 69-78, 2006.- [52] O. Maréchal, P. Poizat, and J.-C. Royer, "Checking Asynchronously Communicating Components Using Symbolic Transition Systems,"
Proc. OTM Confederated Int'l Conf. Move to Meaningful Internet Systems: CoopIS, DOA, and ODBASE, pp. 1502-1519, 2004.- [53] K.L. McMillan,
Symbolic Model Checking. Kluwer Academic Publishers, 1993.- [54] G. Memmi and G. Roucairol, "Linear Algebra in Net Theory,"
Proc. Advanced Course on General Net Theory of Processes and Systems: Net Theory and Applications, vol. 84, pp. 213-223, 1980.- [55] P. Merino and J.M. Troya, "Modeling and Verification of the ITU-T Multipoint Communication Service with SPIN,"
Proc. Int'l SPIN Workshop, 1996.- [56] T. Murata, "Petri Nets: Properties, Analysis and Applications,"
Proc. IEEE, vol. 77, no. 4 pp. 541-580, 1989.- [57] T. Nakatani, "Verification of Group Address Registration Protocol Using PROMELA and SPIN,"
Proc. Third SPIN Workshop, http://spinroot.com/spin/Workshops/ws97nakatani.pdf , 1997.- [58] T.M. Parks, "Bounded Scheduling of Process Networks," PhD thesis, Dept. of Electrical Eng. and Computer Sciences, Univ. pf California, 1995.
- [59] D. Peled, "Ten Years of Partial Order Reduction,"
Proc. 10th Int'l Conf. Computer Aided Verification, vol. 1427, pp. 17-28, 1998.- [60] P. Poizat, J.-C. Royer, and G. Salaün, "Bounded Analysis and Decomposition for Behavioural Descriptions of Components."
Proc. Eighth IFIP WG 6.1 Int'l Conf. Formal Methods for Open Object-Based Distributed Systems, pp. 33-47, 2006.- [61] J. Röder and F.-S. Preiss., "A Promela Model of the Session Initiation Protocol," student project report, ETH Zurich, Dec. 2008.
- [62] P. Romano, M. Romero, B. Ciciani, and F. Quaglia, "Validiation of the Sessionless Mode of the HTTPR Protocol,"
Formal Techniques for Networked and Distributed Systems, pp. 62-78, 2003.- [63] A.W. Roscoe, "Model-Checking CSP,"
A Classical Mind: Essays in Honour of C.A.R. Hoare, chapter 21, Prentice-Hall, 1994.- [64] L.E. Rosier and H.-C. Yen, "Boundedness, Empty Channel Detection, and Synchronization for Communicating Finite Automata."
Theoretical Computer Science, vol. 44, pp. 69-105, 1986.- [65] A. Schrijver,
Theory of Linear and Integer Programming. John Wiley & Sons, Inc., 1986.- [66] B. Selic, G. Gullekson, and P.T. Ward,
Real-Time Object-Oriented Modeling. John Wiley & Sons, 1994.- [67] B. Selic and J. Rumbaugh, "Using UML for Modeling Complex Real-Time Systems," http://www.ibm.com/developerworks/rational/ library139.html, Mar. 1998.
- [68] S.F. Siegel and G.S. Avrunin, "Improving the Precision of INCA by Eliminating Solutions with Spurious Cycles,"
IEEE Trans. Software Eng., vol. 28, no. 2, pp. 115-128, Feb. 2002.- [69] M.H. ter Beek, M. Massink, D. Latella, and S. Gnesi, "Model Checking Groupware Protocols,"
Proc. Cooperative Systems Design, Scenario-Based Design of Collaborative Systems, pp. 179-194, 2004.- [70] F. Tip, "A Survey of Program Slicing Techniques,"
J. Programming Languages, vol. 3, no. 3, pp. 121-189, 1995.- [71] M.N. Wegman and F.K. Zadeck, "Constant Propagation with Conditional Branches,"
ACM Trans. Programming Languages and Systems, vol. 13, no. 2 pp. 181-210, 1991.- [72] W. Wei, "Incomplete Property Checking for Asynchronous Reactive Systems," PhD Thesis, Dept. of Computer and Information Science, Univ. of Konstanz, http://kops.ub.uni-konstanz.de/volltexte/ 20085360/, 2008.
- [73] H.-C. Yen, "A Unified Approach for Deciding the Existence of Certain Petri Net Paths,"
Information and Computation, vol. 96, no. 1, pp. 119-137, 1992. |