ВЕРИФИКАЦИЯ МОДЕЛЕЙ СИСТЕМ НА БАЗЕ ЭКВАЦИОНАЛЬНОЙ ХАРАКТЕРИСТИКИ ФОРМУЛ CTL

Описание

Аннотация

В статье предложена и рассмотрена RTL-нотация, основанная на системах рекурсивных уравнений и привычных семантических определениях логики линейного времени LTL и логики ветвящегося времени CTL. В предыдущих работах авторов, когда данная нотация еще называлась RLTL-нотацией, было показано, что с ее помощью можно легко формулировать и верифицировать свойства логики линейного времени, в том числе и относительно моделей систем, заданных с помощью той же нотации. Затем были расширены возможности RLTL-нотации, благодаря чему с ее помощью стало возможным формулировать выражения не только логики LTL, но и логики ветвящегося времени. В результате этого появилась первая версия RTL-нотации. В данной статье представлена вторая версия RTL как результат доработки и упрощения семантических определений нотации, позволивших повысить наглядность и читаемость ее выражений. Целью статьи является демонстрация возможности использования RTL-нотации в качестве инструмента для формулировки и верификации свойств, задаваемых формулами обеих логик, на базе единых аксиом и правил. Это дает возможность RTL выступать в роли единой универсальной нотации данных логик. При этом за счет незначительных дополнений ее базовых определений нотация способна включать в себя выразительные особенности и других временных логик, что в перспективе позволит RTL стать полноценной универсальной временной логикой, обладающей всеми необходимыми инструментами и средствами для реализации всех этапов верификации.The paper proposes and examines the RTL notation based on systems of recursive equations and standard Linear Temporal Logic (LTL) semantic definitions and the Computational Tree Logic (CTL). When this notation was still called RLTL, the previous works of the authors showed that it enables easy formulation and verifying of LTL properties with respect to system models, even with those that are al-so specified using the RLTL notation. Then the authors expanded the capabilities of the RLTL notation, so it has become possible to formulate LTL and CTL expressions. Therefore, the first version of the RTL notation was created. This article presents the second version of the RTL, which was the result of refinement and simpli-fication of notation semantic definitions, which allowed increasing the visibility and readability of its expressions. The purpose of the article is to demonstrate the possibility of using the RTL notation as a tool to formulate and verify properties defined by formulas of both LTL and CTL logics using common axioms and rules. This lets RTL to become a single and universal notation for these logics. At the same time, it is possible for RTL to include expressiveness of other temporal logics too by minor additions to its basic definitions. It means that in future it is possible for RTL to become a full-fledged universal temporal logic that has all of the necessary tools and means for implementing all stages of verification.