Interactive method for cumulative analysis of software formal models behavior

A.V. Kolchin


The aim of the proposed method is to simplify and improve the process of models debugging and to increase efficiency of model-based test cases generation. Unlike existing methods of models behavior analysis, which produce as a result only one, usually first-found, path per specified property (which is an evidence of test goal reachability or explanation of some inconsistency during debugging process), the
proposed method generates a projection of all satisfiable paths, which provokes exposure of undesired behavior. For test cases generation, the feature plays a role of interactive path constructor, which prompts all satisfiable behavior alternatives, so user can find a desired path by iteratively specifying points-of-interest. Appropriate novel algorithm for efficient searching is presented.

Problems in programming 2018; 2-3: 115-123


testing; debugging; model checking

Full Text:



Marinescu R., Kaijser H. and oth. Analyzing Industrial Architectural Models by Simulation and Model-Checking. Formal Techniques for Safety-Critical Systems. 2014. P. 189-205.

Hessel A., Petterson P. A global algorithm for model-based test suite generation. Electr. Notes Theor. Comp. Sci. 2007. Vol. 190. P. 47-59.

Rushby J. Automated test generation and verified software. Verified Software: Theories, Tools, Experiments. 2008. P. 161-172.

Pasareanu C., Visser W., and oth. Symbolic PathFinder: integrating symbolic execution with model checking for Java bytecode analysis. Automated Software Engineering. 2013. Vol. 20(3). P. 391-425.

Konighofer R., Hofferek G., Bloem R. Debugging formal specifications: a practical approach using model-based diagnosis and counterstrategies. Int. J. on Software Tools for Technology Transfer. 2013. Vol. 15. P. 563-583.

Heimdahl M., Devaraj G., Weber R. Specification test coverage adequacy criteria = specification test generation inadequacy criteria? In IEEE Computer society, HASE. 2004. P. 178-186.

Palomba F., Panichella A., and oth. Automatic Test Case Generation: What if Test Code Quality Matters? In proc. of Int. Symp. on Software Testing and Analysis. 2016. P. 130-141.

Kolchin A.V. Instrumental Tool Design for Asynchronous System Formal Model Testing, Cand. Sci. (Phys.-Math.) Dissertation, Kiev. 2009. 142 P. (in Russian: Razrabotka instrumentalnykh sredstv dlya proverki formalnykh modeley asinkhronnykh sistem: Dis.... kand. fiz.-mat. nauk).

Kolchin A. Directed search in verification of formal models. Theory and Application of Software System Development (TAAPSD'2007). 2007. P. 256-258.

Kolchin A., Kotlyarov V., Drobintsev P. A method of the test scenario generation in the insertion modelling environment. Control systems and machines. 2012. P. 43-48.

Kolchin A.V. An automatic method for the dynamic construction of abstractions of states of a formal model. Cybernetics and Systems Analysis. 2010. Vol. 46. Issue 4. P. 583-601.

Guba A., Kolchin O., Potiyenko S. A method for business logic extraction from legacy COBOL code of industrial systems.



  • There are currently no refbacks.