Integration of verification methods for program systems. (English. Russian original) Zbl 1183.68378

Program. Comput. Softw. 35, No. 4, 212-222 (2009); translation from Programmirovanie 35, No. 4 (2009).
Summary: An approach to constructing an extensible framework for the verification of program systems is suggested. In the author’s opinion, it will facilitate application of modern rigorous verification methods to practically significant programs, the complexity of which permanently grows. This framework can also become a test harness for testing and adjustment of new techniques of formal verification and static analysis on various industrial software packages.


68Q60 Specification and verification (program logics, model checking, etc.)
Full Text: DOI


[1] Maraia, V., The Build Master: Microsoft’s Software Configuration Management Best Practices, Addison-Wesley Professional, 2005.
[2] Robles, G., Debian Counting. http://libresoft.dat.escet.urjc.es/debian-counting/ .
[3] McConnell, S., Code Complete, Microsoft Press, 2004.
[4] Kulyamin, V.V., Software Verification Methods, Vserossiiskii konkurs obzorno-analiticheskikh statei po prioritetnomu napravleniyu ”Informatsionno-telekomunikatsionnye sistemy” (All-Russian Competition of Analytic Survey Papers on Priority Direction ”Information-Telecomunication System”) 2008. http://window.edu.ru/window/library?p_rid=56168 .
[5] Detlefs, D.L., Leino, K.R.M., Nelson, G., and Saxe J.B., Extended Static Checking, Tech. Report SRC-RR-159, Digital Equipment Corporation, Systems Research Center, 1998.
[6] Flanagan, C., Leino, K.R.M., Lillibridge, M., Nelson, G., Saxe, J.B., and Stata, R., Extended Static Checking for Java, Proc. of ACM SIGPLAN 2002 Conf. on Programming Language Design and Implementation, 2002, pp. 234–245.
[7] Cok, D.R. and Kiniry, J.R., ESC/Java2: Uniting ESC/Java and JML, Lecture Notes in Computer Science (Proc. of Int. Workshop on the Construction and Analysis of Safe, Secure, and Interoperable Smart Devices (CASSIS’04)), Springer, 2005, vol. 3362, pp. 108–128.
[8] Barnett, M., Chang, B.-Y.E., DeLine, R., Jacobs, B., and Leino, K.R.M., Boogie: A Modular Reusable Verifier for Object-Oriented Programs, Lecture Notes in Computer Science (Proc. of Formal Methods for Components and Objects), 2005, vol. 4111, Springer, 2006, pp. 364–387.
[9] Xie, Y. and Aiken, A., Saturn: A Scalable Framework for Error Detection Using Boolean Satisfiability, ACM Transactions Programming Languages Systems (Proc. of Principles of Programming Languages (POPL 2005)), ACM, 2007, vol. 29, no. 3.
[10] Babic, D. and Hu, A.J., Calysto: Scalable and Precise Extended Static Checking, Proc. of the 30th Int. Conf. on Software Engineering, 2008, pp. 211–220.
[11] Ball, T. and Rajamani, S.K., Automatically Validating Temporal Safety Properties of Interfaces, Lecture Notes in Computer Science (Proc. of Model Checking of Software), Springer, 2001, vol. 2057, pp. 103–122. · Zbl 0985.68641
[12] Miné, A., The Octagon Abstract Domain, Higher-Order Symbolic Computation, 2006, vol. 19, no. 1, pp. 31–100. · Zbl 1105.68069
[13] Clarke, E., Grumberg, O., Jha, S., Lu, Y., and Veith, H., Counterexample-Guided Abstraction Refinement, Lecture Notes in Computer Science (Proc. of CAV 2000), Springer, 2000, vol. 1855, pp. 154–169. · Zbl 0974.68517
[14] Emanuelsson, P. and Nilsson, U., A Comparative Study of Industrial Static Analysis Tools, Tech. Report 2008:3, Linkoping University, 2008. http://www.ep. liu.se/ea/trcis/2008/003/trcis08003.pdf .
[15] http://www.mathworks.com/products/polyspace/index.html .
[16] Blanchet, B., Cousot, P., Cousot, R., Feret, J., Mauborgne, L., Mine, A., Monniaux, D., and Rival, X., Design and Implementation of a Special-purpose Static Program Analyzer for Safety-critical Real-time Embedded Software The Essence of Computation: Complexity, Analysis, Transformation. Essays Dedicated to Neil D. Jones, Schmidt, D.A. and Sudborough, I.H., Eds., Lecture Notes in Computer Science, Springer, 2002, vol. 2566, pp. 85–108. · Zbl 1026.68514
[17] Souyris, J. and Delmas, D., Experimental Assessment of ASTRÉE on Safety-Critical Avionics Software, Lecture Notes in Computer Science (Proc. of Int. Conf. on Computer Safety, Reliability, and Security, SAFECOMP 2007), Saglietti, F. and Oster, N., Eds., Nuremberg, Germany, Springer, 2007, vol. 4680, pp. 479–490.
[18] Henzinger, T.A., Jhala, R., Majumdar, R., and Sutre, G., Software Verification with Blast, Lecture Notes in Computer Science (Proc. of the 10-th SPIN Workshop on Model Checking Software (SPIN 2003)), Springer, 2003, vol. 2648, pp. 235–239. · Zbl 1023.68532
[19] Chaki, S., Clarke, E., Groce, A., Jha, S., and Veith, H., Modular Verification of Software Components in C, IEEE Trans. Software Engineering, 2004, vol. 30, no. 6, pp. 388–402. · Zbl 05113895
[20] Godefroid, P., Klarlund, N., and Sen, K., DART: Directed Automated Random Testing, Proc. of 2005 ACM SIGPLAN Conf. on Programming Language Design and Implementation, ACM, 2005, pp. 213–223.
[21] Godefroid, P., Compositional Dynamic Test Generation, Proc. of the 34-th Annual ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages (PLOP 2007), 2007, pp. 47–54.
[22] Sen, K., Agha, G., CUTE and jCUTE: Concolic Unit Testing and Explicit Path Model-checking Tools, Proc. of Comput. Aided Verification, 2006, pp. 419–423.
[23] Smaragdakis, Y. and Csallner, C., Check ’n’ Crash: Combining Static Checking and Testing, Proc. of the 27-th ACM/IEEE Int. Conf. on Software Engineering (ICSE), 2005, pp. 422–431.
[24] Smaragdakis, Y. and Csallner, C., Combining Static and Dynamic Reasoning for Bug Detection, Lecture Notes in Computer Science (Proc. of TAP 2007), Springer, 2007, vol. 4454, pp. 1–16.
[25] Xie, T., Marinov, D., Schulte, W., and Notkin, D., Symstra: A Framework for Generating Object-Oriented Unit Tests using Symbolic Execution, Proc. of the 11th Int. Conf. on Tools and Algorithms for the Construction and Analysis of Systems (TACAS 2005), Edinburgh, 2005, pp. 365–381. · Zbl 1087.68601
[26] Tillmann, N. and Schulte, W., Parameterized Unit Tests with Unit Meister, ACM SIGSOFT Software Engineering Notes, 2005, vol. 30, no. 5, pp. 241–244.
[27] Tillmann, N. and de Halleux, J., Pex–White Box Test Generation for.NET, Lecture Notes in Computer Science (Proc. of TAP 2008), Springer, 2008, vol. 4966, pp. 134–153.
[28] Cadar, C., Ganesh, V., Pawlowski, P.M., Dill, D.L., and Engler, D.R., EXE: Automatically Generating Inputs of Death, Proc. of the 13th ACM Conf. on Comput. and Communications Security, Alexandria, Virginia, USA, 2006, pp. 322–335.
[29] Pacheco, C., Lahiri, S.K., Ernst, M.D., and Ball, T., Feedback-Directed Random Test Generation, Proc. of Int. Conf. on Software Engineering, 2007, pp. 75–84.
[30] Model Based Testing of Reactive Systems, Lecture Notes in Computer Science, Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., and Pretschner, A., Eds., Springer, 2005, vol. 3472.
[31] Utting, M. and Legeard, B., Practical Model-Based Testing: A Tools Approach, Morgan-Kaufmann, 2007.
[32] Jacky, J., Veanes, M., Campbell, C., and Schulte, W., Model-Based Software Testing and Analysis with C#, Cambridge University, 2007. · Zbl 1142.68024
[33] Kulyamin, V.V., Petrenko, A.K., Kosachev, A.S., and Burdonov, I.B., The UniTesk Approach to Designing Test Suites, Programmirovanie, 2003, no. 6, pp. 25–43 [Programming Comput. Software (Engl. Transl.), 2003, vol. 29, no. 6, pp. 310–323].
[34] Hartman, A., Model Based Test Generation Tools, AGEDIS Project, 2002. http://www.agedis.de/docu-ments/ModelBasedTestGenerationTools.pdf .
[35] Korel, B., Automated Test Data Generation, IEEE Trans. Software Engineering, 1990, vol. 16, no. 8, pp. 870–879. · Zbl 05114234
[36] DeMillo, R. and Offutt, A., Constraint-based Automatic Test Data Generation, IEEE Trans. Software Engineering, 1991, vol. 17, no. 9, pp. 900–910. · Zbl 05114378
[37] Gotlieb, A., Botella, B., and Rueher, M., Automatic Test Data Generation Using Constraint Solving Techniques, ACM SIGSOFT Software Engineering Notes, 1998, vol. 23, no. 2, pp. 53–62.
[38] Gargantini, A. and Heitmeyer, C., Using Model Checking to Generate Tests from Requirements Specifications, Proc. of the Joint 7th European Software Engineering Conf. and the 7-th ACM SIGSOFT Int. Symp. on Foundations of Software Engineering (ESEC/FSE99), ACM, 1999, pp. 146–162.
[39] Hong, H.S., Lee, I., Sokolsky, O., and Cha, S.D., Automatic Test Generation from Statecharts Using Model Checking, Tech. Report MS-CIS-01-07, 2001.
[40] Hamon, G., de Moura, L., and Rushby, J., Generating Efficient Test Sets with a Model Checker, Proc. of the 2nd Software Engineering and Formal Methods Int. Conf., 2004, pp. 261–270.
[41] Beyer, D., Chlipala, A.J., Henzinger, T.A., Jhala, R., and Majumdar, R., Generating Tests from Counterexamples, Proc. of the 26th Int. Conf. on Software Engineering (ICSE), 2004, pp. 326–335.
[42] Lee, I., Kannan, S., Kim, M., Sokolsky, O., and Viswanathan, M., Runtime Assurance Based On Formal Specifications, Proc. of Int. Conf. on Parallel and Distributed Processing Techniques and Applications PDPTA’1999, 1999, pp. 279–287.
[43] Cheon, Y. and Leavens, G.T., A Runtime Assertion Checker for the Java Modeling Language (JML), Proc. of Int. Conf. on Software Engineering Research and Practice (SERP’02), CSREA, 2002, pp. 322–328.
[44] Cavalli, A., Gervy, C., and Prokopenko, S., New Approaches for Passive Testing Using an Extended Finite State Machine Specification, Information Software Technology, 2003, vol. 45, no. 12, pp. 837–852.
[45] Drusinsky, D., Modeling and Verification Using UML Statecharts, Newnes, 2006.
[46] Drusinsky, D., The Temporal Rover and the ATG Rover, Lecture Notes in Computer Science (Proc. of SPIN Workshop 2000), Springer, 2000, vol. 1885, pp. 323–329. · Zbl 0976.68571
[47] Brat, G., Visser, W., Havelund, K., and Park, S., Java PathFinder–Second Generation of a Java Model Checker, Proc. of Workshop on Advances in Verification, Chicago, 2000.
[48] http://javapathfinder.sourceforge.net/ .
[49] Blackburn, M.R., Busser, R.D., and Nauman, A.M., Interface-Driven, Model-Based Test Automation, CrossTalk, J. Defense Software Engineering, 2003.
[50] Artho, C., Barringer, H., Goldberg, A., Havelund, K., Khurshid, S., Lowry, M., Pasareanu, C., Rosu, G., Sen, K., Visser, W., and Washington, R., Combining Test Case Generation and Runtime Verification, Theoretical Comput. Sci., 2005, vol. 336, no. 2–3, pp. 209–234. · Zbl 1080.68062
[51] Brat, G., Havelund, K., Park, S., and Visser, W., Model Checking Programs, Proc. of the 15th IEEE Int. Conf. on Automated Software Engineering, Grenoble, France, 2000, pp. 3–11.
[52] Holzmann, G.J., The SPIN Model Checker: Primer and Reference Manual, Addison-Wesley Professional, 2003.
[53] http://spinroot.com/ .
[54] Blackburn, M., Busser, R.D., and Fontaine, J.S., Automatic Generation of Test Vectors for SCR-style Specifications, Proc. of the 12th Annual Conf. on Comput. Assurance, 1997, pp. 54–67.
[55] http://www.t-vec.com/ .
[56] http://www.microsoft.com/whdc/devtools/tools/SDV.mspx .
[57] Ball, T., Bounimova, E., Cook, B., Levin, V., Lichtenberg, J., McGarvey, C., Ondrusek, B., Rajamani, S.K., and Ustuner, A., Thorough Static Analysis of Device Drivers, ACM SIGOPS Operating Systems Review, 2006, vol. 40, no. 4, pp. 73–85.
[58] Grieskamp, W., Kicillof, N., MacDonald, D., Nandan, A., Stobie, K., and Wurden, F.L., ModelBased Quality Assurance of Windows Protocol Documentation, Proc. of the 1st Int. Conf. on Software Testing, Verification, and Validation, ICST 2008, Lillehammer, Norway, 2008, pp. 502–506.
[59] Veanes, M., Campbell, C., Grieskamp, W., Schulte, W., Tillmann, N., and Nachmanson, L., Model-Based Testing of Object-Oriented Reactive Systems with Spec Explorer. Formal Methods and Testing, Lecture Notes in Computer Science, Springer, 2008, vol. 4949, pp. 39–76. · Zbl 1120.68354
[60] http://research.microsoft.com/en-us/projects/specexpl-orer/ .
[61] http://research.microsoft.com/en-us/um/redmond/gr-oups/rise/ .
[62] Bourdonov, I., Kossatchev, A., Petrenko, A., and Galter, D., KVEST: Automated Generation of Test Suites from Formal Specifications, Lecture Notes in Computer Science (Proc. of FM’99, Toulouse, France), Springer, 1999, vol. 1708, pp. 608–621.
[63] Kuliamin, V., Petrenko, A., and Pakoulin, N., Practical Approach to Specification and Conformance Testing of Distributed Network Applications, Service Availability, Malek, M., Nett, E., Suri, N., Eds., Lecture Notes in Computer Science, Springer, 2005, vol. 3694, pp. 68–83.
[64] Grinevich, A., Khoroshilov, A., Kuliamin, V., Markovtsev, D., Petrenko, A., and Rubanov, V., Formal Methods in Industrial Software Standards Enforcement, Lecture Notes in Computer Science (Proc. of PSI’2006, Novosibirsk, Russia, 2006), Springer, 2006, vol. 4378, pp. 459–469.
[65] Zelenov, S.V., Zelenova, S.A., Kosachev, A.S., and Petrenko, A.K., Test Generation for Compilers and Other Formal Text Processors, Programmirovanie, 2003, no. 2, pp. 59–69 [Programming Comput. Software (Engl. Transl.), 2003, vol. 29, no. 2, pp. 104–112]. · Zbl 1063.68042
[66] Manolios, P., Subramanian, G., and Vroon, D., Automating Component-based System Assembly, Proc. of ISSTA 2007, London, UK, 2007, pp. 61–72.
[67] Poll, E., van den Berg, J., and Jacobs, B., Specification of the JavaCard API in JML, Proc. of CARDIS’00, Kluwer Academic, 2000.
[68] Bouquet, F. and Legeard, B., Reification of Executable Test Scripts in Formal Specification-based Test Generation: The Java Card Transaction Mechanism Case Study, Proc. of the Int. Symp. of Formal Methods Europe, Springer, 2003, pp. 778–795.
[69] Bradley, A.R., Sipma, H.B., Solter, S., and Manna, Z., Integrating Tools for Practical Software Analysis, Proc. of 2004 CUE Workshop, Vienna, Austria, 2004.
[70] Gilb, T. and Graham, D., Software Inspection, Addison-Wesley, 1993.
[71] Porter, A., Siy, H., and Votta, L., A Review of Software Inspections, Tech. Report CS-TR-3552, University of Maryland at College Park, 1995.
[72] Laitenberger, O., A Survey of Software Inspection Technologies, Handbook on Software Engineering and Knowledge Engineering, World Sci., 2002, vol. 2, pp. 517–555.
[73] Demakov, A.V., Object-Oriented Description of Graph Data Structures, Programmirovanie, 2007, no. 5, pp. 261–271 [Programming Comput. Software (Engl. Transl.), 2007, vol. 33, no. 5, pp. 261–272]. · Zbl 1154.68350
[74] Gomanyuk, S.V., An Approach to Creating Development Environments for a Wide Class of Programming Languages, Programmirovanie, 2008, no. 4, pp. 225–236 [Programming Comput. Software (Engl. Transl.), 2008, vol. 34, no. 4, pp. 225–236]. · Zbl 1185.68139
[75] GNU Compiler Collection Internals, http://gcc.gnu.org/onlinedocs/gccint/index.html .
[76] Daum, B., Professional Eclipse 3 for Java Developers, Wrox, 2004. · Zbl 1066.68013
[77] http://www.eclipse.org/ .
[78] Yorsh, G., Ball, T., and Sagiv, M., Testing, Abstraction, Theorem Proving: Better Together! Proc. of ISSTA 2006, Partland, Maine, USA, 2006, pp. 145–156.
[79] Beust, C. and Suleiman, H., Next Generation Java Testing: TestNG and Advanced Concepts, Addison-Wesley Professional, 2007.
[80] http://testng.org/doc/ .
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. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.