Nothing Special   »   [go: up one dir, main page]
Skip to main content
Springer Nature Link
Log in

Integration of verification methods for program systems

  • Published:
Programming and Computer Software Aims and scope Submit manuscript

Abstract

In the paper, 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.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

Explore related subjects

Discover the latest articles, news and stories from top researchers in related subjects.

References

  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.

  12. Miné, A., The Octagon Abstract Domain, Higher-Order Symbolic Computation, 2006, vol. 19, no. 1, pp. 31–100.

    Article  MATH  Google Scholar 

  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.

  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.

  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.

    Chapter  Google Scholar 

  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.

  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.

    Article  Google Scholar 

  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.

  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.

    Article  Google Scholar 

  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.

  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.

    Article  Google Scholar 

  36. DeMillo, R. and Offutt, A., Constraint-based Automatic Test Data Generation, IEEE Trans. Software Engineering, 1991, vol. 17, no. 9, pp. 900–910.

    Article  Google Scholar 

  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.

    Article  Google Scholar 

  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.

    Article  Google Scholar 

  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.

  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.

    Article  MATH  MathSciNet  Google Scholar 

  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.

    Article  Google Scholar 

  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.

  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].

  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.

    Google Scholar 

  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].

  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].

  75. GNU Compiler Collection Internals, http://gcc.gnu.org/onlinedocs/gccint/index.html.

  76. Daum, B., Professional Eclipse 3 for Java Developers, Wrox, 2004.

  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/.

Download references

Author information

Authors and Affiliations

  1. Institute for System Programming, Russian Academy of Sciences, ul. Solzhenitsyna 25, Moscow, 109004, Russia

    V. V. Kuliamin

Authors
  1. V. V. Kuliamin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to V. V. Kuliamin.

Additional information

Original Russian Text © V.V. Kuliamin, 2009, published in Programmirovanie, 2009, Vol. 35, No. 4.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Kuliamin, V.V. Integration of verification methods for program systems. Program Comput Soft 35, 212–222 (2009). https://doi.org/10.1134/S0361768809040057

Download citation

  • Received:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1134/S0361768809040057

Keywords

Search

Navigation