×

Model checking merged program traces. (English) Zbl 1347.68244

Machado, Patricia D. L. (ed.), Proceedings of the 11th Brazilian symposium on formal methods (SBMF 2008) Salvador, Brazil, August 26–29, 2008. Amsterdam: Elsevier. Electronic Notes in Theoretical Computer Science 240, 97-112 (2009).
Summary: During a program’s execution, state information can be collected and stored in the form of program traces. With such traces, one can analyze dynamic properties of the program. In this paper, we consider the problem of merging multiple traces from the same program in order to compose an approximate temporal model of its behavior. With such a model one can perform model checking based on both linear- and branching-time logics. To this end, we formally define what we mean by program trace and present some algorithms to perform trace merging. We show that each of these algorithms yield a different kind of temporal model, appropriate for different kinds of analyses. Our method is motivated by the possibility of analyzing simulations in a way that has not been done so far, and thus is developed with the needs of such a domain in mind. To demonstrate the practical feasibility of the proposed theoretical approach, we explain how to actually perform model checking of our temporal models using the NuSMV tool. Moreover, we provide proof-of-concept Java implementations of the proposed trace merging algorithms, which output NuSMV specifications. We also describe a simple case study using this implementation.
For the entire collection see [Zbl 1280.68029].

MSC:

68Q60 Specification and verification (program logics, model checking, etc.)
68N30 Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.)
PDFBibTeX XMLCite
Full Text: DOI

References:

[1] Ammons, G.; Bodík, R.; Larus, J. R., Mining specifications, SIGPLAN Not., 37, 4-16 (2002) · Zbl 1323.68361
[2] Bartetzko, D., C. Fischer, M. Moller and H. Wehrheim, Jass - java with assertions; Bartetzko, D., C. Fischer, M. Moller and H. Wehrheim, Jass - java with assertions
[3] Boigelot, B.; Godefroid, P., Automatic synthesis of specifications from the dynamic observation of reactive programs, (TACAS ’97: Proceedings of the Third International Workshop on Tools and Algorithms for Construction and Analysis of Systems (1997)), 321-333
[4] Burdy, L., Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. Leavens, K. Leino and E. Poll, An overview of JML tools and applications; Burdy, L., Y. Cheon, D. Cok, M. Ernst, J. Kiniry, G. Leavens, K. Leino and E. Poll, An overview of JML tools and applications
[5] Cho, H.; Hachtel, G.; Macii, E.; Plessier, B.; Somenzi, F., Algorithms for approximate FSM traversal based on state space decomposition, IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 15, 1465-1478 (1996)
[6] Cimatti, A.; Clarke, E.; Giunchiglia, E.; Giunchiglia, F.; Pistore, M.; Roveri, M.; Sebastiani, R.; Tacchella, A., NuSMV Version 2: An OpenSource Tool for Symbolic Model Checking, (Proc. International Conference on Computer-Aided Verification (CAV 2002). Proc. International Conference on Computer-Aided Verification (CAV 2002), LNCS, vol. 2404 (2002)) · Zbl 1010.68766
[7] Clarke, E. M.; Emerson, E. A., Design and synthesis of synchronization skeletons using branching-time temporal logic, (Logic of Programs, Workshop (1981)), 52-71
[8] Ernst, M.D., “Dynamically Discovering Likely Program Invariants,” Ph.D. thesis, University of Washington (2000); Ernst, M.D., “Dynamically Discovering Likely Program Invariants,” Ph.D. thesis, University of Washington (2000)
[9] Ernst, M. D.; Perkins, J. H.; Guo, P. J.; McCamant, S.; Pacheco, C.; Tschantz, M. S.; Xiao, C., The Daikon system for dynamic detection of likely invariants, Science of Computer Programming, 69, 35-45 (2007) · Zbl 1161.68390
[10] Finkbeiner, B.; Sipma, H., Checking finite traces using alternating automata, Form. Methods Syst. Des., 24, 101-127 (2004) · Zbl 1073.68053
[11] Geilen, M., On the construction of monitors for temporal logic properties, Electr. Notes Theor. Comput. Sci., 55 (2001)
[12] Gilbert, N.; Bankers, S., Platforms and methods for agent-based modeling, Proceedings of the National Academy of Sciences of the United States, 99 (2002)
[13] Lo, D., S.-C. Khoo and C. Liu, Mining temporal rules from program execution traces3rd International Workshop on Program Comprehension through Dynamic Analysis (PCODA’07); Lo, D., S.-C. Khoo and C. Liu, Mining temporal rules from program execution traces3rd International Workshop on Program Comprehension through Dynamic Analysis (PCODA’07)
[14] Luke, S.; Cioffi-Revilla, C.; Panait, L.; Sullivan, K., Mason: A new multi-agent simulation toolkit (2004), paper and toolkit are available at
[15] Meyer, B., Applying “design by contract”, Computer, 25, 40-51 (1992)
[16] North, M.; Collier, N.; Vos, J. R., Experiences creating three implementations of the repast agent modeling toolkit, ACM Transactions on Modeling and Computer Simulation, 16, 1-25 (2006), toolkit is available at
[17] Pnueli, A., The temporal logic of programs, (18th IEEE FOCS (1977)), 46-57
[18] (2007), Sun Microsystems, Java technology
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.