基于惰性切片的线性时态逻辑性质验证

惰性切片是一种有效的状态空间缩减方法,但是它无法直接判定一个模型是否满足所期望的线性时间性质。针对该问题,提出了一种基于惰性切片的线性时态逻辑公式验证方法。该方法首先构造给定线性时态逻辑公式的否定Büchi自动机与系统模型的乘积自动机,然后使用惰性切片算法在该乘积自动机上以惰性方式搜索可接受迹,从而把线性时间性质验证问题转换为通过可达性分析搜索可接受状态的不变性检测过程。实验结果证明,基于惰性切片的线性时态逻辑公式验证算法在不损失验证结果正确性的前提下使惰性切片算法具备了验证线性时间性质的能力,同时也有效提高了LTL模型检测方法的可扩展性。     

区间时序逻辑的模型检查

为了检验标注有限状态自动机描述的系统是否满足某个区间时序逻辑公式刻画的性质,定义了一套转换规则．利用这些规则,可以构造一个chop-自动机,该自动机接受的语言恰是所有满足这个区间时序逻辑公式的模型的集合．同时,定义了一套转换规则把一个chop-自动机转换为一个标注有限状态自动机,使得它们接受相同的原子命题序列集．这样,区间时序逻辑的模型检查问题就等价地转换成了很容易解决的两个标注有限状态自动机的语言包含问题．     

一种基于时态逻辑的有限状态系统验证方法

ＬＰＴＬ与自动机之间有着紧密的联系,结合ＬＰＴＬ语义和语法,提出一种从ＬＰＴＬ公式导出Ｂｕｃｈｉ自动机的方法。导出的Ｂｕｃｈｉ自动机所接受的语言准确地表达了ＬＰＴＬ公式所描述的特性。从而把由ＬＰＴＬ公式描述的系统设计规范的验证问题转换成检验Ｂｕｃｈｉ自动机的包含问题。     

多速率混合系统的模型检查

研究了初始化的多速率混合系统的模型检查问题,即检验初始化的多速率自动机是否满足某个混合区间时序逻辑公式描述的性质．首先定义了一套转换规则把混合区间时序逻辑公式转化为区间时序逻辑公式．接着定义了初始化的多速率自动机状态空间上的等价关系及其对应的域自动机,并且通过构造域自动机对应的标注有限状态自动机,把初始化的多速率混合系统的模型检查问题等价地转换成了可解的区间时序逻辑的模型检查问题．利用区间时序逻辑的模型检查算法加上上述的转换规则,就可以解决初始化的多速率混合系统的模型检查问题．     

模拟抽象思维行为的形式系统

由于一阶语言表达能力的局限性，本文首先在一阶语言的基础上增加一些算子构成新的语言，使语言的表达能力得到增强，并且给出了该语言下公式的语义解释。其次，使用这种语言对诸如信念之类的认知观念进行形式化，然后基于模态逻辑和时态逻辑结构念逻辑；最后基于信念逻辑对Ｄａｖｉｓ－Ｐｕｔｍａｎ方法进行推广来对认知公式进行推理。基于上述四点，提出了一个信念系统模型来模拟抽象思维行为，并在ＶＡＸ－Ⅱ上用ＣＯＭＭＯＮ－Ｌ     

一类约束语言的上限能控子语言进一步讨论

事件与状态为离散事件动态系统的二特征量，状态的逻辑演化关系可用有限自动机模型来描述，系统的逻辑运行特性则为事件集上的事件串（序列）。受禁状态集或（和）受禁事件串集为离散事件动态系统的一类重要性能指标。Ｌｉｎ等对其首先进行了讨论，给出了受禁状态集或（和）受禁事件串集约束语言指标的上限能控子语言及其该指标下离散事件动态系统监控器综合的计算方法。在对该类约束语言的上限能控子语言展开了进一步的讨论同时，修     

协议模型形式描述方法与趋势

本文分析了协议模型形式描述方法(自动机法,Petri-net法,高级语言模型,语义学模型,时态逻辑,代数模型,混合型模型)和特点,并简要介绍了协议形式描述技术的应用和发展趋势。     

基于Spin的地铁门控制系统建模与验证

针对地铁门控制系统(MDCS)安全问题,提出一种MDCS检测方法。通过分析MDCS的控制逻辑,使用Promela建立了基于Spin的MDCS系统模型,将MDCS中的地铁控制系统、地铁门控制系统及屏蔽门控制系统抽象为三个进程,并用线性时态逻辑公式描述待验证性质,运行Spin后即可判断MDCS是否存在安全隐患。实验结果表明,该检测方法可有效验证MDCS的安全性。     

面向自动化设备的行为监测与异常诊断措施

根据自动化设备行为检测中的不足,采取相应的异常诊断措施,通过有限状态自动机作为自动化设备的行为监测与异常诊断的基础,对自动化设备分为多个模块相结合的状态,并通过多个模块相结合的状态来辨别自动化是否正常运行以及转换的状态,并将得到的设备运行状态模型还原设备运行过程。除此之外,该措施还能将事前设置好的设备行为状态模型与状态变换、设备状态以及等待测试的设备指令进行对比,得出的结果就可以知道设备运行过程中是否存在异常行为。最后研究结果表明,该措施能有效的对自动化设备进行行为监测与异常诊断。     

基于HLA的复杂产品协同设计中数据一致性

通过分析复杂产品协同设计的特点和高层体系结构(high level architecture,简称HLA)在工程设计领域中的应用,构建了一种基于HLA的联邦式协同设计系统体系结构,阐述了系统中各平台的组成和功能.为确保协同设计过程中联邦成员收发数据的一致性,提出了各平台中联邦成员的时间管理策略,给出了系统整体时间推进的方法和过程.在时间管理策略的基础上,通过采用设置内部和外部事件逻辑计数器方法和基于仲裁的锁定机制,实现了系统运行过程中设计邦员动态注册的初始一致性.     

Constructing formal verification models for hardware Trojans

The effectiveness of hardware security verification is affected by the way of constructing formal verification models.To solve this problem,this paper proposes a method which can automatically construct formal verification models for hardware Trojans detection.First,the method traverses the control flow graphs of the register transfer level design to extract the path conditions of assignment statements and the corresponding expressions.The constraint relations of the Kripke’ state transition are generated based on the path conditions and the expressions.Second,the constraint relations of the Verilog grammar are transformed to the grammar of the model checker and generate the formal verification models.Finally,a model checker verifies the models and detects the hardware Trojans when a predefined specification is verified as false.In experiments,the hardware Trojans in the Trust-HUB benchmarks are detected,which shows that the models constructed by our method can effectively detect hardware Trojans in register transfer level design.     

Propositional projection temporal logic based distributed model checking method

To alleviate the state-explosion problem of model checking, a novel distributed model checking method based on the propositional projection temporal logic (PPTL). First, the property to be verified in the PPTL formula is transformed into an automaton with the technique of Labeled Normal Form Graph, which in turn is partitioned into multiple subautomata according to the strongly connected components. Then, each subautomaton and the system model in the Hierarchical Syntax Chart are delivered to the members of the verification server cluster, and model checking of the system is implemented in parallel with the on-the-fly technique on multiple computers. Experimental results indicate that, compared with the standalone model checking approach, the proposed method can not only significantly reduce the time consumption but also verify more complex systems.     

A unified linear-time temporal logic solution to the steam-boiler control specification problem

The TLL XYZ/E is a formal language able to represent the dynamic semantics and the static semantics in a unified framework. It supports the whole process of program development, i.e. from the abstract specification to the efficiently executable program in a formal, precise and convenient way. The steam boiler control specification problem, a large case study in the fields of real time, hybrid and communication systems, is discussed with XYZ/E. The approach covers physical model construction, formal specification, stepwise refinement, verification, executable program and visual user interface programming.     

进位保留加法器的命题投影时序逻辑组合验证

为保证硬件设计的正确性,提出了对硬件设计组合验证的新方法．该方法在命题投影时序逻辑的统一框架下,实现对硬件系统行为的建模,对所期望性质的形式化描述,并利用命题投影时序逻辑合理且完备的公理系统对系统性质进行验证,从而证明硬件系统满足期望的性质,保证设计的正确性．进位保留加法器的验证实例说明了该方法的可行性．     

SOC的形式化验证方法

如何对片上系统(SOC)来进行验证,是一个比较复杂的问题。本文介绍了用形式化方法来验证SOC,讨论在对SOC进行等价性验证时应注意的几个问题以及解决的方法。最后给出了对SOC验证的一般方法。     

UML statechart based rigorous modeling of real-time system

Rigorous modeling could ensure correctness and could verify a reduced cost in embedded real-time system development for models. Software methods are needed for rigorous modeling of embedded real-time systems. PVS is a formal method with precise syntax and semantics defined. System modeled by PVS specification could be verified by tools. Combining the widely used UML with PVS, this paper provides a novel modeling and verification approach for embedded real-time systems. In this approach, we provide 1 ) a time-extended UML statechart for modeling dynamic behavior of an embedded real-time system ; 2) an approach to capture timed automata based semantics from a timed statechart; and 3 ) an algorithm to generate a finite state model expressed in PVS specification for model checking. The benefits of our approach include flexibility and user friendliness in modeling, extendability in formalization and verification content, and better performance. Time constraints are modeled and verified and is a highlight of this paper.     

MSVL程序的自动定理证明方法

The MSVL is a temporal logic programming language. It can be used to verify C, Verilog/VHDL programs. To do so, a program written in C or Verilog/VHDL is translated to an MSVL program, and then the task is changed to verify MSVL programs. However, at present, the correctness of MSVL programs can only be proved by hand with deductive approaches. This is tedious and error-prone. To handle this problem, an automatic theorem proving technique for the MSVL based on the interactive theorem prover PVS is proposed. To this end, first the syntax and semantics of the MSVL are described in the specification language of PVS, which enables MSVL programs to be correctly recognized by PVS. Further, an axiomatic system of the MSVL and some theorems are specified. Then the proof commands of PVS are input for invoking the PVS prover to deduce MSVL programs. During verification, simple details can be proved by PVS automatically while complex steps are controlled by human. In this way, MSVL programs can be verified semi-automatically, which facilitates the deduction of MSVL programs. An instance of the bakery algorithm is given to show that our method is feasible.     

基于PVS的飞机订票系统的形式化描述与验证

形式化方法主要应用于安全性第一的系统的规范与形式验证。原型证明系统PVS为开发和分析形式化规范和验证提供了一个集成化环境。本文介绍PVS系统的证明方法和特点 ,并利用PVS系统对飞机订票系统的需求给出了形式化规范 ,对部分关键属性完成了证明 ,说明了使用PVS系统的某些经验和技巧     

投影时序逻辑的公理系统与形式验证

为了采用定理证明的方法对并发及交互式系统进行验证,提出了一阶投影时序逻辑的公理系统．利用投影时序逻辑既可描述待验证系统性质和规范,又可描述其实现模型的特点,在同一投影时序逻辑框架可以方便地对待验证系统进行建模和性质描述,并使用公理系统完成系统性质的证明．最后通过一个实例来展示投影时序逻辑及公理系统在系统验证中的应用．     

对离散事件系统的共可诊断性验证

提出了一种验证离散事件系统共可诊断性的多项式算法,算法通过构建一个检验自动机来实现,将故障路径和正常路径提取出来进行对比。另外将传统的共可诊断性划分为两种情况分别处理可以提高算法效率。可分别用于验证系统的F-共可诊断性和NF-共可诊断性。复杂性分析和案例分析表明本文算法的计算复杂度更低。实验验证了本文方法的高效性和有效性。