TLC model checking and the concurrency in specification

Abstract

Розглянуто метод перевірки на моделі TLC. Проведено дослідження відповідних часових витрат. У проведеному дослідженні розглянуто темпоральні специфікації композитного веб- сервісу з елементами паралелізму. Порівняно два підходи до верифікації (перевірки на моделі) – BFS- та DFS-орієнтований.The TLC Model Checker has been considered. The investigation of corresponding time costs has been conducted. In the case study conducted the Composite Web Service temporal specifications with concurrency have been considered. Two approaches to model checking have been compared – the breadth-first-search- and the depth-first-search-based.