Штучний інтелект

Науковий журнал

ISSN 2710-1673

ONLINE: ISSN 2710-1681

Шукати за:

Роком видання
Автором
Назвою статті

A static method for elimination of redundant dependencies in preconditions of transitions of formal models of transition systems

Колчін А.В.1, Летичевский А.А.2, Потієнко С.В.1
1 V.M. Glushkov Institute of Cybernetics of the National Academy of Sciences of Ukraine
2 V.M. Hlushkov Institute of cybernetics NAS of Ukraine

Повний текст (PDF)

УДК: 004.832.23+004.942
Мова публікації: Російська
Stuc. intelekt. 2015; 20; (1-2):127-136

Анотація: Мета запропонованого методу – скоротити простір, що досліджується, поведінки формальних моделей, та, як наслідок, підвищити ефективність аналізу її властивостей. В основі методу лежить алгоритм статичного символьного аналізу передумов переходів моделі.

Ключові слова: верифікація, редукція простору пошуку, інформаційна залежність.

Посилання:

  1. Jhala R., Majumdar R. Software model checking // ACM Comput. Surv. – Vol.41(4). – 2009. – 54 P.
  2. 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.
  3. 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.
  4. Holzmann G. The model checker SPIN // IEEE transactions on software engineering. – 1997. – Vol. 23. –N 5. – P. 279–295.
  5. 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.
  6. 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.
  7. Halder R. Cortesi A., Abstract program slicing on dependence condition graphs Science of ComputerProgramming Volume 78, Issue 9, 1 September 2013, Pages 1240–1263.
  8. Ilan Beer, Shoham Ben-David and oth. Explaining Counterexamples Using Causality // Formal Methodsin System Design. – 2012. – №40. – P. 20–40.
  9. 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.
  10. Kolchin A. V., Chetvertak R.V. An interactive system for analysis of formal models behavior // Artificialintelligence. –2012. – №4. – P. 330–341.
  11. 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.
  12. Dijkstra E. Guarded commands, nondeterminacy and formal derivation of programs // Communicationsof the ACM. – 1975. – Vol.18. – N 8. – P. 453–457.
  13. 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.

Переглянути повний текст статті (PDF)