UML Statecharts的切片模型检验方法

Slicing UML Statecharts for Model Checking

统一建模语言UML已被广泛应用于软件设计和开发中,而验证UML模型是否满足关键的性质需求成为一个重要问题.由于空间爆炸和语义的复杂性,对Statecharts进行模型检验受到软件规模和设计精化程度的制约.本文在用扩展层次自动机(EHA)结构化的表示UML Statecharts后,通过分析EHA中存在的层次、并发和事件同步等特征定义了一组依赖关系.对于由状态和迁移组成的切片准则,给出对EHA进行切片的算法.该算法能保证切片后的EHA与原来的Statecharts对性质具有相同的可满足性,且删除了与被验证性质无关的层次和并发状态,缓解了空间爆炸问题.

Unified Modeling Language (UML) has been widely used in software development. Verifying whether a UML model meets the reared properties has become a challenge. Model checking is an important technology of automatic verification to ensure the correctness of designed models. Because of space explosion and complicated semantics, model checking Statecharts are restricted by the software scale and the refinement degree of design. In this paper, UML Statecharts are structurally expressed by Extended Hierarchical Automaton (EHA). A set of dependence relations is specified after analyzing the characteristics such as hierarchy, concurrency and synchronization in EHA. The algorithm of slicing EHA based on the slicing criterion which is composed by states and transitions is presented. The sliced EHA and the original Statecharts are equivalent to the property.The algorithm removes the hierarchies and concurrent states which are irrelevant with the property, and reduce the state space efficiently.