A method for guided search and test scenarios generation in verification of formal models of asynchronous systems

A.V. Kolchin

Abstract


A guided search method for automatic test scenario building during verification proposed. The method uses user-defined regular expressions as test purposes and for model behavior traversal bounding. Search managing strategies together with trace and state equivalence weakening described.

Problems in programming 2008; 4: 4-12


References


http://en.wikipedia.org/wiki/Model_checking

Ben-Ari. M. Principles of Spin. // Springer Verlag. – 2008. – P. 216.

Burch J., Clarke E., McMillan K., Dill D., and Hwang L. Symbolic model checking: 10^20 states and beyond // Information and Computation. – 1992. – Vol. 98, N 2. – P. 142–170.

Cimatti A., Clarke E., Giunchiglia E., and others. NuSMV 2: An OpenSource Tool for Symbolic Model Checking // In Proceeding of International Conf. on Computer-Aided Verification, Copenhagen, Denmark. – 2002. – P. 359–364.

Godefroid P. Partial-order methods for the verification of concurrent systems – an approach to the state-explosion problem // Lecture notes in computer science, Springer-Verlag. – 1996. – Vol. 1032. – P. 143.

ITU-T Recommendation Z.100 – Specification and Description Language (SDL), ITU. – 2002.

ISO/IEC. Information Processing Systems - Open Systems Interconnection – LOTOS – A Formal Description Technique based on the Temporal Ordering of Observational Behaviour. ISO/IEC 8807:1989, International Organization for Standardization, Geneva, Switzerland. – 1989.

ISO/TC97/SC21. Information Processing Systems – Open Systems Interconnection – Estelle – A Formal Description Technique based on an Extended State Transition Model. ISO 9074:1997, International Organization for Standardization, Geneva, Switzerland. –1997.

Fernandez J., Jard C., Jeron T., Nedelka L., and Viho C. An experiment in automatic generation of test suites for protocols with verification technology // Science of Computer Programming. – 1997. – Vol. 29, N 1–2. – P. 123–146.

Grabowski J., Hogrefe D., Nahm R. Test case generation with test purpose specification by MSCs // In Elsevier Science B.V. (North-Holland), editor, 6th SDL Forum. – 1993. – P. 253–266.

ITU-T Recommendation Z.120 – Message Sequence Chart (MSC), ITU. – 1996.

Bourdonov I., Kossatchev A., Kuliamin V., and Petrenko A. UniTesK Test Suite Architecture // In Proc. of FME 2002, LNCS 2391, Springer-Verlag. – 2002. – P. 77–88.

Колчин А.В. Направленный поиск в верификации формальных моделей // Тези доп. Міжнар. конф. «Теоретичні та прикладні аспекти побудови програмних систем TAAPSD'2007» – К.: НаУКМА, Національний ун-т ім. Т.Г. Шевченка, Інститут програмних систем НАН України. – 2007. – С. 256–258.

Баранов С.Н., Котляров В.П., Летичевский А.А. Индустриальная технология автоматизации тестирования мобильных устройств на основе верифицированных поведенческих моделей проектных спецификаций требований // Труды Междунар. науч. конф. «Космос, астрономия и программирование» – С-Пб: СПбГУ. – 2008. – С. 134–145.

Aho A. Algorithms for finding patterns in strings // Handbook for theoretical computer science, MIT Press. – 1990. – Vol. A. – P. 257–300.

Smyth B. Computing Patterns in Strings // ACM Press Books. – 2003. – P. 440.

Колчин А.В. Автоматический метод оперативного построения абстракций при верификации формальных моделей асинхронных систем // Искусственный интеллект. – 2008. – N 4. – P. 690–705.

Clarke E. Model checking and abstraction // In ACM Transactions on programming languages and systems. – 1994. – Vol. 16, N 5. – P. 1512–1542.

Bloem R., Ravi K., and Somezi F. Symbolic guided search for CTL model checking // In Design Automation Conference. – 2004. – P. 29–34.

Barner S., Glazberg Z., and Rabinovitz I. Wolf - bug hunter for concurrent software using formal methods // In Computer Aided Verification. – 2005. – P. 153–157.

Peranandam P., Weiss R., Ruf J., Kropf T. and Rosenstiel W. Dynamic guiding of bounded property checking // In IEEE International High Level Design Validation and Test Workshop. – 2004. – P. 15–18.

Edelkamp, S., Leue S., and Lafuente A. L. Directed explicit-state model checking in the validation of communication protocols // International journal on software tools for technology transfer. – 2003. – N 5. – P. 247–267.

Baranov S.N., Kapitonova J.K., Kolchin A.V., and others. Tools for Requirements Capturing Based on the Technology of Basic Protocols // Proc. of St. Petersburg IEEE Chapter. – 2005. – P. 92–97.


Refbacks

  • There are currently no refbacks.