摘要：跨时钟域(Clock Domain Crossing,CDC)设计和验证是SOC系统芯片设计的关键问题。讨论了异步FIFO的模型检验方法,利用模型检验工具SMV,建立了异步FIFO的有限状态机模型,使用时序逻辑ltl对该模型和属性进行了描述和验证。实验结果达到要求,同时表明该方法是行之有效的。与传统的模拟和仿真等验证方法相比较,模型检验具有能够自动进行、验证速度快、不用书写测试激励等优点。

摘要：测试预言是一种用来检测被测系统的测试执行是否正确的方法。文中,作者设计并实现了一种根据程序的线性时序逻辑(ltl)的性质产生测试预言的方法。首先,作者将一线性时序逻辑公式转换为一个有限状态自动机,然后,管理源代码,以便抽取与线性时序逻辑性质有关的状态序列。最后,用该信息来模拟状态自动机,并决定程序执行是否满足线性时序逻辑的性质。

摘要：UML是一种通用的图形化建模语言,在面向对象系统的分析与设计中,形成了一个统一的、公共的、具有广泛适用性建模语言,但它并不是形式化的建模语言,缺乏精确的表示语义,表达不严格。线性时序逻辑(ltl)是一种形式化语言,是并发或反应式程序动态语义,适合用来精确表示模型的动态语义。本文介绍UML的形式化建模方法,详细描述线性时序逻辑语言的语法及语义,并将形式化建模方法用在图书管理系统中。

摘要：模型检测是一种有着自动化并能提供反例的验证系统属性的形式化分析方法,其由系统模型,系统属性的描述和模型检测器组成。模型检测器接受模型和属性自动的去验证属性是否满足模型,如果不满足给出一个反例,其在软硬件验证中都得到了广泛的应用。模型检测器SPIN是由贝尔实验室开发的一种适合于并发系统的模型检测工具。本文在介绍了SPIN的设计和结构,分析了其理论基础,并通过具体例子阐述了安装和使用模型检测器SPIN和它的图形化界面iSpin的使用方法。SPIN接受Promela语言建立的模型和使用线性时序逻辑ltl描述的性质,给出验证结果。本文在研究模型检测工具SPIN的结构和原理的基础上,详细的阐述了其图形化界面iSpin的安装和使用。

摘要：在智能轨道交通中,信号系统作为指挥列车安全运行的核心控制系统,在列车运行过程中,控制不当可能导致对人类生命,财产或环境造成灾难性后果。传统的自然语言描述使系统开发缺乏统一的标准,而形式化方法可以有效验证和评估系统设计正确性。文章研究了形式化安全保障技术在智能轨道交通领域的应用,针对全自动驾驶FAO系统中各子系统之间复杂的交互作用,文章结合了形式化方法和STPA方法。以车载ATP系统为例,进行形式化和安全分析方法的结合分析,按照STPA步骤进行安全分析,识别系统相关的安全约束,并运用了XSTAMPP软件辅助分析过程。研究结果实现了自然语言的安全需求到线性时序逻辑(ltl)的形式化规范的转化,有效避免了可能存在的二义性,体现了STPA与形式化结合方面的实际应用价值,并为接下来进行形式化验证提供参考。