Static method of consistency and completeness checking in formal model of distributed software systems
Abstract
The paper describes a new method for discovering of incompleteness, inconsistency and race conditions in formal models. The method implements the properties checking basing on model transitions description, and does not traverse model state space.
Prombles in programming 2014; 2-3: 145-150
Full Text:
PDF (Русский)References
Колчин А.В., Летичевский А.А, Потиенко С.В. и др. Обзор современных систем и методов верификации формальных моделей // Проблеми програмування. – 2012. – № 4. – С. 59–72.
http://www.klocwork.com
Flanagan C., Freund S. FastTrack: efficient and precise dynamic race detection // ACM SIGPLAN Notices - PLDI '09. – 2009. – Vol. 44. –
P. 121–133.
Voung J., Jhala R., Lerner S. Relay: static race detection on millions of lines of code // In Proc. of the the 6th joint meeting of the European
software engineering conference and the ACM SIGSOFT symposium on the foundations of software engineering. – 2007. – P. 205–214.
Летичевский А.А. (мл.). Об одном классе базовых протоколов // Проблеми програмування. – 2005. – № 4. – С. 3–19.
Потиенко С.В. Статическая проверка требований и подходы к решению проблемы достижимости // Искусственный интеллект. – 2009. – № 1. – С. 192–197.
Potiyenko S. Static verification of basic protocols systems with unbounded number of agents // 3rd International Workshop SCSS 2010, Symbolic Computation in Software Science, Hagenberg, Austria, July 29-03. – 2010. – P. 51–54.
Naik M., Aiken A., Whaley J. Effective static race detection for Java. // Doctorial thesis, Stanford University Stanford, CA, USA. –161P. –2008.
Netzer R., Miller B. On the complexity of event ordering for shared-memory parallel program executions // Int. conf. On parallel processing. – 1990. – P. 1193–1197.
Летичевский А.А., Годлевский А.Б. и др. Свойства предикатного трансформера системы VRS // Кибернетика и системный анализ. –
– № 4. – С. 3–16.
Refbacks
- There are currently no refbacks.