模型检验是一种非常重要的自动验证方法，主要通过显式状态搜索或隐式不动点计算来验证有穷状态系统的模态命题性质，避免建立复杂的证明过程，并在不满足性质时能提供反例。二十多年来，人们对它进行了广泛而深入的研究，取得了许多研究成果，使得它在软硬件验证等方面得到广泛应用，受到了广大研究和开发人员的高度重视。 本文主要针对Statecharts及其时间扩展的形式化验证进行研究，研究工作包括：(1)通过对Statecharts和模型检验理论的研究，给出了平坦化和非平坦化的模型检验算法；(2)基于抽象解释框架的性质强保留的抽象模型检测；(3)把图形化的 Statecharts转换为义本表示的Statetxt，从而演绎验证Statecharts；(4)对连续时间扩展的Statecharts模型检验进行了研究和探索。主要成果表现在以下几个方面： ⑴通常模型检验Statecharts是先对其平坦化，然后使用已有模型检验工具进行验证。本文对传统的 Statecharts模型检验方法进行了改进，提出了一种针对Statecharts语义的平坦化模型检验方法。该方法基于Statecharts的操作语义和statecharts到LTS转换规则，得到标签转换系统LTS；在此基础上，对LTS进行符号表示，然后基于导向集的前向状态搜索算法，符号检验Statecharts模型是否满足CTL公式的性质。通过状态搜索的导向集和状态空间的符号表示，比较有效的缩减了需验证的状态窄间。为了进一步解决状态空间爆炸问题，又提出了一种非平坦化的模型检验方法，基于自动机理论及Statecharts的操作语义，避免构造平坦化过程，缩减状念窄间体积，并通过可达性分析和环路检测，直接对分层的Statecharts进行模型检验，验证其线性时态逻辑性质。非平坦化的方法能避免因Statecharts平坦化而引起的状态空间爆炸问题。 ⑵为了进一步研究Statecharts平坦化的模型检验方法，基于抽象解释的理论，以及完备抽象解释和性质强保留之间的关系，提出了一种性质强保留的抽象模型检验方法。此方法根据抽象解释中抽象域的最小完备精化，来获得CTL性质强保留的最优抽象模型，并且最优抽象模型总是存在。首先通过状态标签函数确定初始抽象域，然后通过不动点求解，得到对补集和标准前向转换完备的最优抽象域，也就是对CTL标准算子完备的最小抽象域，依据此抽象域求解CTL性质强保留的最优抽象状态划分。在抽象状态划分之间定义抽象转换关系，构造CTL性质强保留的抽象模型。并指出了抽象域对CTL标准算子是完备的当且仪当抽象域对补集和标准前向转换是完备的。此方法比较有效的解决了状态空间爆炸问题。 ⑶为了自动演绎验证Statecharts，需对图形化的Statecharts转换为文本表示Statetxt，然后进行验证。本文提出了一种在演绎验证不变式中辅助不变式的自动生成方法。描述了一个生成不变式和辅助谓词的框架，从而验证时态安全性质。为了保证搜索的收敛，通过对系统安全抽象来构造近似系统。该方法为形式化验证Statecharts提供了一种新的思路。 ⑷为了使Statecharts能描述连续时间的能力，本文精确定义了连续时间扩展的时间Statecharts，并提出了一种模型检验时间Statecharts的方法。采用项代数表示时间Statecharts和进程代数描述其并发行为，根据其一步语义及转换规则，把时间Statecharts映射为时间自动机，从而对时间Statecharts模型检的问题转换为对时间自动机的模型检验。为了克服了连续时间的无穷问题，通过抽象技术来获得有限状态空间，并给出了抽象精化的算法。