Search by:
Year of publication
Author name
Paper title
A static method for elimination of redundant dependencies in preconditions of transitions of formal models of transition systems
Full text (PDF)
UDC: 004.832.23+004.942
Publication Language: Russian
Stuc. intelekt. 2015; 20(1-2):127-136
Abstract: The objective of the proposed method is to reduce search space in the behavior of formal models, and, as a consequence, to increase efficiency of model checking. The core of the method is an algorithm of static symbolic analysis of preconditions of model transitions.
Keywords: model checking, state space reduction, data dependency.
References:
- Jhala R., Majumdar R. Software model checking // ACM Comput. Surv. – Vol.41(4). – 2009. – 54 P.
- Peled D. Partial order reduction: linear and branching temporal logics and process algebras // In proc. ofthe workshop on Partial order methods in verification. NY, USA: AMS Press, Inc. – 1997. – P. 233–257.
- Godefroid P. Partial-order methods for the verification of concurrent systems – an approach to the state–explosion problem // LNCS, Springer-Verlag. – 1996. – Vol. 1032. –143 P.
- Holzmann G. The model checker SPIN // IEEE transactions on software engineering. – 1997. – Vol. 23. –N 5. – P. 279–295.
- Podgurski A., Clarke A. A. Formal model of program dependencies and its implications for softwaretesting, debugging and maintenance // IEEE Trans. Software Eng. – 1990. –Vol.16(9). –P. 965–979.
- Cortesi A., Halder R. Dependence Condition Graph for Semantics-based Abstract Program Slicing // InProc. of the 10th Workshop on Language Descriptions, Tools and Applications. – 2010. – №4. – 9 P.
- Halder R. Cortesi A., Abstract program slicing on dependence condition graphs Science of ComputerProgramming Volume 78, Issue 9, 1 September 2013, Pages 1240–1263.
- Ilan Beer, Shoham Ben-David and oth. Explaining Counterexamples Using Causality // Formal Methodsin System Design. – 2012. – №40. – P. 20–40.
- Kolchin A. V. An automatic method for the dynamic construction of abstractions of states of a formalmodel // Cybernetics and system analysis. – 2010. – № 4. – P. 70–90.
- Kolchin A. V., Chetvertak R.V. An interactive system for analysis of formal models behavior // Artificialintelligence. –2012. – №4. – P. 330–341.
- Kolchin A. V. A method for reduction of analyzed behavior space during verification of formal models ofdistributed software systems // Artificial intelligence. –2013. – №4. – P. 113–126.
- Dijkstra E. Guarded commands, nondeterminacy and formal derivation of programs // Communicationsof the ACM. – 1975. – Vol.18. – N 8. – P. 453–457.
- A. Kolchin, A. Letichevsky, S. Potiyenko. Static method of consistency and completeness checking informal model of distributed software systems // Problems in programming. –2014. –N 2–3. –P.146–150.