Verification of Compliance for Multilevel Models in Individual Trace Semantics

Abstract

The paper considers the problem of verification of compliance between models representing the same system on different level of abstraction. The existing approaches are mostly based on refinement relation. But the models representing industrial systems are quite big and complex, while semantics gap between the level is quite big. As a result, the existing methods became too complex and labour intensive. The paper presents new verification techniques that targets to prove multimodel compliance in terms of individual trace semantics. The techniques assume that each model is verified, i.e. it is proved that starting from initial states of labelled transition system is not possible to reach unsafe states by using valid transitions. The first proposed technique allows to prove that the detailed model satisfies to requirements of the abstract model, i.e. reachable states of detailed model do not include states corresponding to unsafe states of the abstract model. The second proposed technique allows to prove that the detailed model satisfies to behaviour specification of the abstract model, i.e. all reachable transitions of the detailed model do not include transitions corresponding to invalid transitions of the abstract model. For each technique the correspondence relation is defined in terms of the models, i.e. the relations are formally defined and they can be used for analysis with interactive or automated provers. At the same time, there are some requirements to that relations that are expressed in terms of low level events that exist hypothetically only and can be analyzed theoretically only. As a result, the proposed techniques provides a reasonable approach to prove compliance between mulilevel models in more approachable way for industrial settings.