模型检验产生于20世纪80年代初，由美国的clarke和Emerson提出的。主要思想是：将要验证的系统抽象为有限状态机，用时态逻辑描述系统应该满足的性质，然后遍历有限状态机的状态空间，对每个状态判断是否满足这些性质，若不满足，将给出一个不满足性质的状态序列，其优点是：全自动进行无须人机交互。近年来，把模型检测应用于软件架构，已成为一个重要方向。因为对于一般的软件系统的状态图中状态是可枚举的，所以我们借鉴模型检测的EMC(显示模型检验)方法，结合状态图的特点研究出SEMC(状态图显示模型检验)。因为软件系统复杂，对象较多，状态图也非常复杂，所以为了使状态图结构清晰，降低复杂性，我们引入层次自动机。