Survey on modern tools and methods of formal models verification
Abstract
A survey on methods for automatic verificatoin of formal models of software systems is presented. Verifiable properties, methods of reduction and modern verification tools are considered.
Keywords
Full Text:
PDF (Русский)References
Brooks F. No Silver Bullet – Essence and Accidents of Software Engineering // Proc. of the IFIP10–th World Computing Conf. – 1986. – P. 1069–1076.
Nelson M., Clark J., Spurlock M. Curing the Software Requirements And Cost Estimating Blues // Program manager. – 1999.
Rashinkara P., Paterson P., Singh L. System-on-a-Chip Verification – Methodology and Techniques // Kluwer Academic Pub-lishers. – 2001. – 392 P.
Boehm B., Basili V. Software Defect Re-duction Top 10 List // IEEE Computer. – 2001. – Vol. 34(1). – P. 135–137.
Hoare T. The verifying compiler: A grand challenge for computing research // J. ACM. – 2003. – Vol. 50(1). – P. 63–69.
Hoare C.A.R. An axiomatic basis for com-puter programming // Communications of the ACM. – 1969. – Vol. 10, N 12. – P. 576–585.
Floyd R. Assigning meaning to programs // Proc. of Symposium in App. Mathematics // J.T. Schwartz, ed. Mathematical Aspects of Computer Science. – 1967. – Vol. 19. – P. 19–32.
Nipkow T., Paulson L., Wenzel M. Isa-belle/Hol: a proof assistant for higher–order logic // LNCS 2283, Springer–Verlag. – 2002. – 218 p.
Owre S., Shankar N. Writing PVS Proof Strategies // Design and application of strategies/ Tactics in Higher Order Logics. – 2003. – P. 1–15.
http://www.klocwork.com
Кулямин В. Методы верификации программного обеспечения // Всероссийский конкурсный отбор обзорно аналитических статей по приоритетному направлению "Информационно телекоммуникационные системы". – 2008. – 117 с.
http://en.wikipedia.org/wiki/Model_checking
http://awards.acm.org/homepage.cfm?srt=all&awd=140
Emerson E. Temporal and modal logic // J. van Leeuwen editor: Handbook of Theoret-ical Computer Science, Elsevier. – 1990. – P. 997–1072.
Wolfgang T. Automata on infinite objects // Handbook of theoretical computer science. – 1990. – P. 133–191.
Sistla A., Vardi M., Wolper P. The com-plementation problem for Buchi automata with application to temporal logic // Theo-retical Computer Science. – 1987. – N 49. – C. 217–237.
Barner S., Glazberg Z., and Rabinovitz I. Wolf – bug hunter for concurrent software using formal methods // In Computer Aided Verification. – 2005. – P. 153–157.
Ben–Ari. M. Principles of Spin // Springer Verlag. – 2008. – 216 p.
Beyer D., Henzinger T., Jhala R., Majumdar R. The software model checker BLAST // Int. J. Software Tools Technol Transfer. – 2007. – N 9. – P. 505–525.
Bloem R., Ravi K., and Somezi F. Symbolic guided search for CTL model checking // In Design automation conference. – 2004. – P. 29–34.
Burch J., Clarke E., McMillan K., and oth. Symbolic model checking: 10^20 states and beyond // Information and Computa-tion. – 1992. – Vol. 98, N 2. – P. 142–170.
Chaki S. A Counterexample Guided Abstraction Refinement Framework for Veri-fying Concurrent C Programs // Doctoral Thesis. Carnegie Mellon University. – 2005. – P. 253.
Cimatti A., Clarke E. M., Giunchiglia E., and oth. NuSMV 2: An Open-Source Tool for Symbolic Model Checking // In Proc. of Int. Conf. on Computer–Aided Verifica-tion, Copenhagen, Denmark. – 2002. – P. 359–364.
Clarke E., Grumberg O., Jha S. et al. Counterexample–guided abstraction re-finement // Computer Aided Verification. – 2000. – P. 154–169.
Clarke E., Grumberg O., Jha S., and oth. Counterexample-guided abstraction refinement for symbolic model checking // Journal of the ACM. –2003. – Vol. 50. – № 5. – P. 752–794.
Clarke E., Jain H., Kroening D. Verification of SpecC using predicate abstraction // Formal Methods in System Design. – 2007. – Vol. 30. – P. 5–28.
Clarke E., Kroening D., Lerda F. A tool for checking ANSI–C programs // Tools and Algorithms for the Construction and Anal-ysis of Systems / Ed. by K. Jensen, A. Po-delski. LNCS 2988. – 2004. – P.168–176.
Dams D. Abstraction in software model checking: principles and practice (Tutorial) // In Proc. of SPIN'02, LNCS 2318. – 2002. – P. 14 -21.
McMillan K. Symbolic Model Checking // Kluwer Academic Publishers. – 1993. – 216 p.
Бурдонов И., Косачев А., Пономаренко В., Шнитман В. Обзор подходов к верификации распределенных систем. – М.: ИСПРАН. – 2006. – 61 с.
Jhala R., Majumdar R. Software model checking // ACM Comput. Surv. – 2009. – Vol. 41(4). – 54 p.
Карпов Ю.Г. Model Checking. Верифи-кация параллельных и распределенных программных систем. – БХВ-Петербург. – 2010. – 552 с.
http://spinroot.com/spin/workshops/index.html
Минский М. Вычисления и автоматы. – М.: Мир, 1971. – 368 с.
Henzinger T., Jhala R., Majumdar R., and Sutre G. Lazy abstraction // In Proc. of the 29th ACM Symposium on Principles of Programming Languages. – 2002. – Vol. 37. – P. 58–70.
Jain H., Kroening D., Sharygina N., and Clarke E. VCEGAR: Verilog counterexam-ple guided abstraction refinement // In Tools and Algorithms for the Construction and Analysis of Systems '07. – 2007. – 4 p.
Летичевский А.А., Годлевский А.Б., Ле-тичевский А.А. (мл.), Потиенко С.В., Песчаненко В.С. Свойства предикатного трансформера системы VRS. // Киберне-тика и системный анализ. – 2010. – № 4. – С. 3–16.
Bryant R. Graph–based algorithms for Boolean function manipulation // IEEE Transactions on Computers. – 1986. – Vol. 35. –P. 677–691.
Pnueli A. The temporal logic of programs // In proc. of the 8th IEEE Symposium on Foundation of Computer Science. – 1977. – P. 46–57.
http://en.wikipedia.org/wiki/Linear_temporal_logic
http://en.wikipedia.org/wiki/Computational_tree_logic
Peled D. Combining partial order reductions with on-the-fly model checking // J. of Formal Methods in System Design. – 1996. – Vol. 8(1). – P. 39–64.
Gerth R., Kuiper R., Peled D., Penczek W. A partial order approach to branching time logic model checking // Information and Computation. – 1999. – Vol. 150(2). – P. 132–152.
Godefroid P. Partial-order methods for the verification of concurrent systems – an ap-proach to the state–explosion problem // Lecture notes in computer science, Spring-er-Verlag. – 1996. – Vol. 1032. –143 p.
Godefroid P. Software model checking: the VeriSoft approach // Formal methods in system design, Springer science. – 2005. – Vol. 26. – P. 77–101.
Peled D. Partial order reduction: linear and branching temporal logics and process al-gebras // POMIV '96: Proc. of the DIMACS workshop on Partial order methods in veri-fication. NY, USA: AMS Press, Inc. – 1997. – P. 233–257.
Apt K., Kozen D. Limits for automatic veri-fication of finite-state concurrent systems // Information Processing Letters. – 1986. – Vol. 22. – P. 307–309.
Ip C., Dill D. Better Verification through Symmetry // Formal Methods in System Design. – 1996. – Vol. 9. – P. 41–75.
Ip C., Dill D. Verifying Systems with Rep-licated Components in Murphi // Int. Conf. on Computer-Aided Verification. – 1996. – P. 147–158.
Miller A., Donaldson A., and Calder M. Symmetry in temporal logic model check-ing // ACM Comput. Surv. – 2006. – Vol. 38. – 37 p.
Nilsson M. Structural Symmetry and Model Checking // Ph.D. thesis, Uppsala Universi-ty, Uppsala, Sweden. – 2005. – 157 p.
Holzmann G. The SPIN Model Checker: Primer and Reference Manual. – Addison-Wesley Professional. – 2003. – 596 p.
Kurshan R. Computer-Aided Verification of Coordinating Processes // Princeton Uni-versity Press. – 1994. – 270 p.
Gupta A., Wang C., Kim H. Hybrid CEGAR: combining variable hiding and predicate abstraction // Proc. IEEE/ACM Int. Conf. on computer-aided design. – 2007. – P. 310–317.
Kesten Y., Pnueli A. Control and data ab-straction: The cornerstones of practical formal verification // Int. J. on Software Tools for Technology Transfer. – 2000. – Vol. 2(4). – P. 328–342.
Lind–Nielsen J., Andersen H., Behrmann G. and oth. Verification of large state/event systems using compositionality and de-pendency analysis // Journal of Formal Methods in System Design. – 2001. – Vol. 18(1). – P. 5–23.
Krinke J. Program Slicing // In Handbook of software engineering and knowledge en-gineering. – Vol. 3. – 2005. – P. 307–332.
Годлевский А.Б. Предикатные трансформеры в контексте символьного моделирования транзиционных систем // Кибернетика и системный анализ. – 2010. – № 4. – С. 91–99.
Колчин А.В. Автоматический метод динамического построения абстракций состояний формальной модели // Кибернетика и системный анализ. – 2010. – № 4. – С. 70–90.
Clarke E. Grumberg O., Long D. Model checking and abstraction // In ACM Transactions on programming languages and systems. – 1994. – Vol. 16(5). – P. 1512–1542.
Jussila T. On Bounded Model Checking of Asynchronous Systems // Doctoral Thesis. Helsinki University of Technology, Laboratory for Theoretical Computer Science. Research report A97. – 2005. – 136 p.
Ball T. A theory of predicate–complete test coverage and generation // In FMCO'2004: Symp. on Formal Methods for Components and Objects. SpringerPress. – 2004. – P. 1–22.
Holzmann G. An analysis of bitstate hash-ing // Formal Methods in Systems Design. – 1998. – P. 301–314.
Peranandam P., Weiss R., Ruf J., Kropf T. and Rosenstiel W. Dynamic guiding of bounded property checking // In IEEE In-ternational High Level Design Validation and Test Workshop. – 2004. – P. 15–18.
Bourdonov I., Kossatchev A., Kuliamin V., and Petrenko A. UniTesK Test Suite Archi-tecture // In Proc. of FME 2002, LNCS 2391, Springer-Verlag. – 2002. – P. 77–88.
Grabowski J., Hogrefe D. SDL and MSC-Based Specification and Automated Test Case Generation for INAP // Telecommu-nication Systems J. – 2002. – Vol. 20(3,4). – P. 265–291.
Летичевский А.А., Колчин А.В. Генерация тестовых сценариев на основе формальной модели // Проблеми програмування. – 2010. – № 2–3. – С. 209–215.
Edelkamp, S., Leue S. and Lafuente A. Directed explicit-state model checking in the validation of communication protocols // International j. on software tools for technology transfer. – 2003. – N 5. – P. 247–267.
Lafuente A. Directed Search for the Verifi-cation of communication protocols // PhD thesis, University of Freiburg. – 2003. – 157 p.
http://nusmv.irst.itc.it
http://www.cs.cmu.edu/~modelcheck/vcegar
http://mtc.epfl.ch/software–tools/blast
http://research.microsoft.com/slam
http://www.cs.cmu.edu/~modelcheck/cbmc
Refbacks
- There are currently no refbacks.