形式验证中同步时序电路的VHDL描述到S2-FSM的转换

符号模型检查（ＳｙｍｂｏｌｉｃＭｏｄｅｌＣｈｅｃｋｉｎｇ,ＳＭＣ）是一种有效的形式验证方法．该方法主要有２个难点：一个是建模,即如何建立并用有限内存来表示电路的状态机模型;另一个是在此模型基础上的验证算法．由于验证时间和有限状态机模型的大小是直接相关的,因而模型的大小就成为ＳＭＣ中的关键问题．本文提出一种基于同步电路行为描述的新的有限状态机模型Ｓ２－ＦＳＭ,并给出从同步电路的ＶＨＤＬ描述建立这种模型的过程．由于该模型的状态转换函数是基于时钟周期的,消去了与时钟无关的大量中间变量,所以同Ｄｅｈａｒｂｅ提出的模型相比,它的状态数大大减少．若干电路的实验结果表明,该模型由于减少了状态规模,建模时间和可达性分析时间大大减少,效果十分显著．     

安全模型的一种形式化方法

本文基于有限状态机的理论，结合通信顺序进行的概念，提出了一种开发安全模型的形式化方法。在该方法中，用ＦＳＭ描述整个系统结构和控制部分，用ＣＳＰ描述系统的状态转移。文章以多级安全策略为例建立了一个安全模型。     

一种n个通信有限状态机的交互式生成法

通信有限状态机是一种直观，易懂且描述能力较强的形式描述工具，它被广泛地用于协议的形式描述，验证及测试、协议变换等，但是，由于描述对象的复杂性和缺少适当的支援工具，ＣＦＳＭ的产生一般依靠手工完成，这除了描述效率低之外，更重要的是所产生的ＣＦＳＭ的性能取于描述人员的习惯、经验，能力等，本文提出了一种由协议文本交互式地产生ｎ个ＣＦＳＭ的生成方法。使用该方法，描述人员可得到ｎ个不包含常见逻辑错误的互相传递     

形式化方法的回顾（续一）

形式化方法的回顾（续一）ＡＲｅｐｏｒｔｆｒｏｍｔｈｅＢＣＳＷｏｒｋｉｎｇＧｒｏｕｐ￥Ｃ．Ｌ．Ｎ．Ｒｕｇｇｉｅｓ（上接１９９３年第３期）２．２并发软件的ＦＤＩ和ＦＳＬ有限状态机（ＦＳＭ：）是用来描述形式系统的语言，曾应用来描述Ａｌｇ。１６０的语法，基于...     

椭圆曲线点乘的抗故障攻击FSM控制器设计

为提高有限状态机(FSM)控制器的抗故障攻击能力,提出一种非并发故障检测方案。方案利用线性码的故障检错特性,通过在状态机电路中建立故障传播路径来实现。设计了基于NAF编码的从左至右扫描点乘算法的安全有限状态机电路,并对该电路进行了仿真验证与分析。通过仿真验证,与并发故障检测方案相比,该设计能够在减少状态机频繁译码工作量的情况下,正确检测错误并报警,提高了抗故障攻击能力。     

基于状态机的ROM接口电路模型

在芯片设计中会经常使用到ROM,而ROM又经常作为片外存储器被所设计的芯片进行读写操作,在这里就需要设计接口电路用来配合ROM和设计的芯片。ROM多为异步工作方式,如果设计的电路为同步电路,之间又存在着接口时序配合的问题。文中介绍一种基于状态机的ROM接口电路模型。该模型有两个特点:一是采用状态机实现同步时序电路与ROM异步时序电路的接口时序配合;二是实现与具有不同时间参数ROM接口电路的兼容。该模型的设计结果通过了FPGA验证,并在ASIC芯片中得到运用。     

基于FSM的协议形式化技术研究

本文主要讨论基于有限状态机(FSM)的协议形式化技术问题。文中论述了FSM形式描述与验证的技术特征,提出了一种增强FSM形式化方法,并给出了基于该方法的形式描述与验证的协议实例。     

基于状态机的ROM接口电路模型

在芯片设计中会经常使用到ROM,而ROM又经常作为片外存储器被所设计的芯片进行读写操作,在这里就需要设计接口电路用来配合ROM和设计的芯片.ROM多为异步工作方式,如果设计的电路为同步电路,之间又存在着接口时序配合的问题.文中介绍一种基于状态机的ROM接口电路模型.该模型有两个特点:一是采用状态机实现同步时序电路与ROM异步时序电路的接口时序配合;二是实现与具有不同时间参数ROM接口电路的兼容.该模型的设计结果通过了FPGA验证,并在ASIC芯片中得到运用.     

基于同步有向图的同步测试序列生成方法

使用多测试单元的测试系统可以对多端口协议实现进行一致性测试，但是在进行这种一致性测试时，测试系统各个端口之间可能会出现同步问题，现在，解决同步问题常用的办法是在测试单元相应端口之间增加同步连接，然后通过此同步连接相互发送同步消息来进行同步，多端口协议和其它类型的分布式系统可以用有限状态机模型来描述，目前，同步问题被分为双端口同步问题，多端口同步问题，紧同步问题等多种类型，该文考虑两种有限状态机测试问题，第一种是面向端口的测试，不考虑有限状态机测试单元之间的通信问题，第二种面向组的测试，有限状态机中的各个端口被分成互不相关的多个组，属于不同组中的测试单元之间互不通信，该文提出了一种基于同步有向图的同步测试序列生成方法，这种生成方法适用于Pair同步，Port同步和组同步问题，并且，这种方法也可以用来判断如何在非同步测试序列中增加同步通信，将非同步测试序列转化为同步测试序列。     

基于SMT的区域控制器同步反应式模型的形式化验证

在安全关键系统的软件开发过程中,形式化验证是一种经检验的提高软件质量的技术.然而,无论从理论上还是从应用角度来看,软件的验证都必须是完整的,数据流验证应该是对实现层软件模型进行验证的必要体现.因此,环境输入、泛型函数、高阶迭代运算和中间变量对于分析形式化验证的可用性至关重要.为了验证同步反应式模型,工程师很容易验证控制流模型(即安全状态机).现有工作表明,这类工作无法全面地验证安全关键系统的同步反应式模型,尤其是数据流模型,导致这些方法没有达到工业应用的要求,这成为对工业安全软件进行形式化验证的一个挑战.提出了一种自动化验证方法.该方法可以实现对安全状态机和数据流模型的集成进行验证.采用了一种基于程序综合的方法,其中,SCADE模型描述了功能需求、安全性质和环境输入,可以通过对Lustre模型的程序综合,采用基于SMT的模型检查器进行验证.该技术将程序合成作为一种通用原理来提高形式化验证的完整性.在轨道交通的工业级应用(近200万行Lustre代码)上评估了该方法.实验结果表明,该方法在大规模同步反应式模型长期存在的复杂验证问题上是有效的.     

针对同步时序电路VHDL设计的有效模型判别器VERIS

介绍了一个针对同步时序电路VHDL设计的性质验证的解决方案-一个有效的符号模型判别器VERIS,该模型判别器利用同步时序电路设计的特点以及待验证性质的局部性,可显著地减少有限状态机（FSM）的状态空间;大大地提高可达性分析和性质验证的速度;同时,实现了反例生成机制,实验结果表明,与Deharbe的模型判别器相比,用这个模型判别器验证一些基准电路更加适用于同步时序电路。     

一种输电线路巡检机器人越障规划方法

针对输电线路巡检机器人的局部自主与远程控制方式,提出了一种基于有限状态机的越障规划方法.将巡检机器人的越障运动过程分解成若干离散化的关键状态,建立了运动规划的有限状态机模型.采用一种基于模糊方法的产生式系统用于推理越障模式,并产生运动序列.仿真与现场实验验证了越障规划方法的正确性和有效性,该方法可应用于输电线路巡检机器人运动控制.     

远程测控模块中有限状态机的设计

基于FPGA无线测控模块在测控系统中有限状态机的设计,通过主从机的工作状态和行为转移的描述,建立以有限状态机为核心模型的远程测控系统,并利用实际硬件模块实现了对温度、溶氧量等现场环境远程测控的真实验证.实际使用结果证实了测控系统中状态机模型的通用性和可靠性,对于基于FPGA的远程测控模块的验证设计具有很好的工程参考价值.     

基于VHDL的有限状态机描述及综合

介绍了使用VHDL描述有限状态机的方法，重点分析了综合过程中的难点并提供了解决方法。最后以乘法电路为例实现了可综合的FSM描述并通过门级仿真验证正确性。     

一种基于有限状态机的模型转换方法

为实现模型的自动转换，通过定义一个清晰的基于规则的模型转换框架，提出了一种基于有限状态机的模型转换方法，用有限状态机技术解决转换规则的实现问题，并定义了适合规则实现机制的形式表示法，然后结合UML模型到SQL模型转换的典型场景，通过一个模型转换示例说明模型转换方法的具体应用，结果表明了该方法的可行性和有效性。该方法适用于状态明显的模型之间的转换，促进了模型自动转换的应用和发展。     

面向仿真训练系统的过程模型研究

该文首先说明了过程模型的功能，根据功能需求对相关过程建模方法进行分析，找出了适合于仿真系统中过程模型的描述方法，并重点给出了一种基于有限状态机方法的训练过程模型框架、过程模型实时调度方法和应用实例。该过程模型框架由演示过程、物理行为过程、混合过程、过程转移、转移条件等对象类组成，在仿真训练系统开发中，通过定义和扩展这些对象类，对基于有限状态机的过程模型进行控制与调度，准确而全面地描述和管理仿真训练过程，从而有效地解决了仿真训练系统中的过程模型开发问题。     

基于UML的计算机联锁软件的分析与建模

有效地测试、分析和验证计算机联锁软件是保证列车运行安全和旅客生命财产安全的重要手段,而形式化模型是系统测试、分析和验证的基础。以联锁软件的UML非形式化模型为基础,以有限状态机模型为系统形式化模型描述的数学工具,研究UML顺序图(场景)自动转化为有限状态机模型的方法。首先将场景的UML顺序图转化为FSP进程代数模型,然后通过合并不同对象的进程代数模型,得到系统的有限状态机模型。最后以接车进路用例为例生成系统的有限状态机模型,以验证该方法的可行性和有效性。     

基于FSM的形式化测试序列生成方法

有限状态机是协议测试序列生成中常用到的数学模型，本文在介绍ＦＳＭ的基础上，总结了国外几种常见的基于ＦＳＭ的测试序列生成技术，并对我们研究中的ＰＡＤ测试序列的生成进行介绍。     

一种协议互操作测试系统开发框架

鉴于现有的协议互操作测试方法自动化程度不高,本文给出一种用于描述分布式通信系统的有限状态机模型,并基于该形式化模型和被动测试的思想提出一种协议互操作测试系统开发框架,遵循该框架开发的测试系统能够自动分析被测系统每次通信从属的协议过程,并自动验证报文和流程的正确性。     

基于Struts的Web程序分析与测试

介绍了Struts的特点、基于Struts框架Web程序的工作流程。分析了基于Struts框架Web程序的动态行为，并提出用有限状态机描述其动态行为。最后根据状态机模型，提出运用T—Method生成Web程序测试路径，结合Struts框架提供的数据验证功能给出了生成测试数据的方法。