中文摘要：

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