Deductive verification of requirements for event-driven architecture

The current paper presents the technology of processing of requirements for systems with event-driven architecture. The technology consists of the stages of formalization, formal verification and conversion to design specifications. The formalization is the formal description of events as formal spe...

Повний опис

Збережено в:
Бібліографічні деталі
Дата:2025
Автори: Letichevsky, A.A., Letichevsky, O.O., Peschanenko, V.S., Guba, A.A.
Формат: Стаття
Мова:English
Опубліковано: PROBLEMS IN PROGRAMMING 2025
Теми:
Онлайн доступ:https://pp.isofts.kiev.ua/index.php/ojs1/article/view/778
Теги: Додати тег
Немає тегів, Будьте першим, хто поставить тег для цього запису!
Назва журналу:Problems in programming
Завантажити файл: Pdf

Репозитарії

Problems in programming
Опис
Резюме:The current paper presents the technology of processing of requirements for systems with event-driven architecture. The technology consists of the stages of formalization, formal verification and conversion to design specifications. The formalization is the formal description of events as formal specifications called basic protocols. The consistency and completeness of basic protocols, safety properties and user-defined properties are verified. The deductive tools for dynamic and static checking are used for detection of properties violation. The method of enlargement allows reducing the complexity of proving and solving. Formal presentation of requirements allows converting them to SDL\UML specifications and generating the test suite. The technology is realized in IMS system and applied in more than 50 projects of telecommunication, networking, microprocessing and automotive systems.Problems in programming 2013; 2: 54-61