Метод статической проверки полноты и непротиворечивости в формальных моделях распределенных программных систем

• Published in: Проблеми програмування
• Date: 2014
• Main Authors: Колчин, А.В., Летичевский, А.А., Потиенко, С.В.
• Format: Article
• Language: Russian
• Published: Інститут програмних систем НАН України 2014
• Subjects: Формальні методи програмування
• Online Access: https://nasplib.isofts.kiev.ua/handle/123456789/113225
• Journal Title: Digital Library of Periodicals of National Academy of Sciences of Ukraine
• Cite this: Метод статической проверки полноты и непротиворечивости в формальных моделях распределенных программных систем / А.В. Колчин, А.А. Летичевский, С.В. Потиенко // Проблеми програмування. — 2014. — № 2-3. — С. 146-150. — Бібліогр.: 10 назв. — рос.

Описан метод выявления таких патологий формальных моделей, как неполнота и противоречивость, а так же гонки в параллельных процессах. Метод реализует проверку свойств на основании анализа описания переходов модели, при этом не строит пространство ее состояний. 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.