由于因特网和嵌入式系统在汽车、飞机以及其它安全系统的成功应用，未来将会更加依赖于计算机设备的功能。由于技术的快速发展，发展验证系统正确性的可靠方法变的越来越重要。目前用于复杂系统的有效方法包括仿真验证、测试验证和形式化验证。前两者验证花费的时间空间长、不易使用，并且无法做到对所有可能性输入和潜在的缺陷进行验证。形式化验证使用数学的方法证明给定的系统模型是否满足要求，从而做到了对用例的全覆盖。形式化验证又包括了形式化等价验证、推理验证和模型验证。模型验证是一种用于验证有限状态并发系统的技术，它对系统建模，并验证系统是否满足规格说明。时序逻辑如 CTL、LTL是目前常用的规格说明语言，基于 CTL、LTL的模型检验广泛应用于工业中。GSTE是一种高效的自动化模型检验算法，使用断言图作为规格说明语言。断言图较时序逻辑更易于使用，而 LTL与断言图在描述方面更为接近，因此，将 LTL转换成断言图有着实用的意义。　　本课题从形式化方法的基本概念出发，对时序逻辑和断言图进行了对比其优劣势，并对断言图进行了扩展，针对课题进一步的扩展，提出了扩展的验证算法，使得算法能够验证扩展之后的断言图并利用其性质验证了算法的正确性和完备性。　　本文首先介绍了形式化方法和模型检验的概念，给出了课题的研究意义，其次详细的介绍了广义符号轨迹赋值的验证过程，引入了其规格说明语言断言图，再次本文介绍了LTL、CTL及基于这些时序逻辑的模型检验算法，对比了CTL与LTL之间的区别和联系，然后对比了 GSTE和基于时序逻辑的模型验证算法，将时序逻辑转换成 Büchi自动机，并将 Büchi自动机转换成断言图，从而达到将时序逻辑转换成 Büchi自动机的形式，在这过程中说明了断言图的局限性。本文基于广义符号轨迹赋值的相关性质引入终端的概念，基于断言图定义了终端断言图，并将强满足算法进行扩展，提出终端可满足性算法，使得其能验证终端断言图，本文给出了终端可满足性的相关性质，并使用数学推理证明了终端可满足算法的正确性和完备性。在文章的最后，通过模型对性质进行验证满足性的过程说明了终端可满足算法的计算过程。