TCBV:一种构件时序行为建模与相容性验证工具

利用形式化方法对复杂实时构件系统的时序行为进行建模与验证对于提高安全攸关实时构件系统的正确性、可靠性与安全性具有重要意义。介绍了基于时间行为协议的构件时序行为的形式化建模和相容性验证方法,给出了时间行为协议建模与相容性验证工具TCBV的系统架构与功能模块。TCBV应用方便,能够实现实时构件时序行为模型的图形化表示,并可对复杂交互行为的相容性进行自动验证。结合应用实例,介绍了如何利用TCBV对复杂实时构件系统的时序行为进行建模和验证。最后,将TCBV与其它相关工具进行了比较。     

穿刺机器人运动安全性的形式化分析与建模

混成系统是实时嵌入式系统的重要子类,其行为中存在连续变化和离散跳转混杂的情况,使得混成系统行为复杂,安全性难以掌握。近年来,混成系统在医疗环境中得到越来越广泛的应用。其中,医疗机器人的穿刺运动控制系统呈现高度复杂的混成性,如果机器人在穿刺过程中失控将导致不可挽回的严重后果。因此穿刺机器人运动行为的安全性设计成为了亟需解决的问题。首先根据穿刺机器人的运动学设计,将机器人的复杂运动分解。然后基于微分动态逻辑理论从混成系统的角度出发对穿刺机器人的运动控制系统进行了形式化建模与分析,并使用证明工具KeYmaera归纳出微分不变式,获得了控制模型的参数约束。最后提出了针对机器人运动到某一靶目标区域这类运动学问题的一般性验证模型。     

基于MARTE的面向混成系统的模型形式化转换

混成系统是离散逻辑跳转与实时连续行为交织的复杂状态变迁系统,形式化建模与验证是确保混成系统正确性和可靠性的重要途径。首先介绍一种混成ZIA形式规范;然后,基于建模语言MARTE建立扩展Object-Z的规范,即OZ-MARTE,该规范弥补了MARTE规范在形式化描述方面的不足,同时为了方便描述混成系统中连续动态行为属性,给出对混成系统中连续变量的描述转换规则,增强了MARTE对混成系统的描述能力;最后,给出OZ-MARTE规范到混成ZIA规范的转换方法,因此针对混成ZIA规范的验证技术同样适用于对MARTE模型进行形式化验证。     

一种面向CPS的控制应用程序协同验证方法

信息-物理融合系统是一种新型嵌入式系统计算模式,它集成了控制计算过程和受控对象,二者相互影响并有机结合.随着信息技术在现实世界中更加广泛、深入的应用,智能化程度不断提升,在具有信息物理紧密耦合特点的嵌入式系统中,嵌入式控制软件的功能比重急剧上升,作用更加突出.作为安全攸关的系统,需要引入形式化验证方法来保证嵌入式控制应用软件的安全性.本文基于自动机理论建立统一的系统验证模型,并针对系统的可达性、安全性（safety）和活性（liveness）等属性要求,提出了对该模型进行形式化验证的算法：基于有界模型检验方法,基于可达性将对系统模型的相关属性验证问题转换为可满足性判定问题.将活性转换为Büchi自动机,并基于四值语义进行判断.在求解过程中,通过偏序规约等手段化简了问题求解的规模,提高可验证系统的规模.另外结合协同仿真技术,灵活配置验证的场景,提高验证的可用性.实验结果表明,结合仿真,形式化协同验证方法可以有效地对系统进行验证.     

基于扩展SysML活动图的嵌入式系统设计安全性验证方法研究

能源、交通等领域中复杂嵌入式系统设计的安全性分析与验证工作已经成为当前的重要研究热点之一;本文提出一种结合MARTE语义信息的扩展Sys ML活动图模型,用于描述安全关键应用中的嵌入式系统动态行为的设计,并对此扩展模型展开基于模型转换的系统设计安全性特征的形式化分析与验证方法的研究;包括:构建了Sys ML活动图与MARTE中非功能性质建模语义相结合的元模型,以及验证工具UPPAAL的时间自动机元模型,并且给出了二者之间的语义映射规则;建立了从时间自动机模型描述到UPPAAL工具输入格式之间的语法转换方法;设计了一个基于AMMA平台的面向扩展Sys ML活动图的模型转换与验证框架;最后,给出了一个高铁控制系统设计模型的安全性验证的实例分析.     

安全的混成系统神经网络控制器生成与验证

控制器生成是混成系统控制中的重要问题.生成具有安全保证的控制器,关系着混成系统在安全攸关领域的使用.提出了一种为混成系统生成具有安全保证的神经网络控制器的方法.神经网络控制器的安全性由与其同时生成的障碍证书保证.为了生成安全的神经网络控制器,首先确定控制器的网络结构,并基于混成系统构造训练数据集;然后,根据保证控制器安全的障碍证书条件编码神经网络训练时的损失函数.当训练完成后,学习到的神经网络控制器对于训练数据集中的数据是安全的,但对于整个混成系统可能并不安全.为了检验学习到的控制器在整个系统上的安全性,将其安全验证问题转化为一组混合整数规划问题,并使用数值优化器求解,以得到形式化保证的结果.工作实现了安全神经网络控制器生成工具SafeNC,并评估了它在8个基准系统上的性能.实验结果表明:SafeNC可以生成包含6个隐藏层的具有1 804个神经元的安全神经网络控制器;同时,与现有方法相比, SafeNC可为更复杂的系统生成安全的神经网络控制器,更有效且更具扩展性.     

嵌入式实时软件模型开发环境研究

为保证嵌入式实时软件的功能安全和实时性,基于模型驱动开发方法,研究了嵌入式实时软件的模型开发环境的体系结构,设计了一个嵌入式实时软件模型开发环境的原型MDE环境.其中应用任务模型使用两层模型机制:上层模型用于建模应用任务的功能行为与性能特征并支持形式化功能安全验证和实时性分析,下层模型用于模型测试和自动生成支持嵌入式实时操作系统API接口和驱动函数接口的应用任务源代码.通过工具集成实现了建模、分析验证、代码生成和测试等嵌入式实时软件的完整模型化开发过程,为将来进一步完善和改进嵌入式实时软件模型开发环境的构建技术提供了应用验证.     

基于XYZ/E的混成系统

混成系统是由计算机和物理设备组成的嵌入式实时计算系统.它允许在交互式实时系统中引入连续变化的单元.XYZ/E 是基于Manna-Pnueli的线性时序逻辑的程序设计语言.它将程序的动态语义与静态语义统一在同一框架中,支持从抽象的程序规范到可执行代码的逐步求精的全过程.该文使用XYZ/E语言描述和验证混成系统.首先介绍了计算模型,然后介绍了XYZ语言对混成系统的形式化描述,最后介绍了混成系统的验证.与同类工作相比,XYZ/E支持状态转换,从而可以方便地描述复杂的控制算法.     

基于Event-B的航天器内存管理系统形式化验证

内存管理系统位于操作系统内核的最底层,为上层提供内存分配和回收机制.在航天器这类安全攸关的关键系统中,其可靠性和安全性至关重要,必须要考虑到强实时性、有限空间限制、高分配效率以及各种边界条件约束.因此,系统通常采用较为复杂的数据结构和算法来管理内存空间,同时需要采用非常严格的形式化方法来保证航天器这类安全攸关系统的高可信性.对复杂内存管理系统的形式化验证也会较之前的验证工作带来更多难题,主要体现在：内存管理模块中的复杂数据结构的形式化描述;操作的规范语义;行为的建模;内部函数的规范及断言定义与循环不变式的定义;实时性验证等方面.本文拟针对这些问题,深入分析实际的航天器操作系统内存管理系统的特性;探索基于分层迭代的语义描述与验证的一般性方法与理论,并应用这些理论方法,来验证一个具有实际应用的航天嵌入式操作系统的内存管理系统.本文研究成果有望被直接应用于我国新一代的航天器系统上.     

模型驱动的嵌入式系统设计安全性验证方法研究

基于模型的嵌入式系统安全性分析与验证方法是近年来在安全攸关系统工程领域中出现的一个重要研究热点。提出一种基于模型驱动架构的面向SysML/MARTE状态机的系统安全性验证方法,具体包括:构建了具备SysML/MARTE扩展语义的状态机元模型,以及安全性建模与分析语言AltaRica的语义模型GTS的元模型;然后建立了从SysML/MARTE状态机模型分别到时间自动机模型以及AltaRica模型的语义映射模型转换规则,并基于AMMA平台和时间自动机验证工具UPPAAL设计实现了对SysML/MARTE状态机的模型转换与系统安全性形式化验证的框架。最后给出了一个飞机着陆控制系统设计模型的安全性验证实例分析。     

Safety assurance in process control

Programmable logic controllers are popular in process-control applications, but the software can be very complex. To make it easier to verify the safety of PLC software, we have created a rigorous process that uses formal specifications of function blocks, which are typically used in safety-critical control and automation applications. Key to the process is the use of Obj, an algebraic language that lets you specify requirements and designs independently of any data representation and implementation. We also used the Obj3 system, which supports the latest version of Obj with an interpreter and a functional programming environment, to automate parts of the specification testing and formal verification     

车站联锁进路控制逻辑的形式化方法

基于计算机联锁系统是一个对列车行驶系统提供安全条件的系统,车站联锁系统是保证车站行车安全和提高运输效率的典型安全苛求性系统。以形式化 方法Event-B为基础,引入角色Agent对联锁系统进行规范定义,通过智能体与Event-B的建模和验证,构造了车站联锁进路控制逻辑形式化验证模型,并进行 了形式化规范和推理,该模型在RODIN平台上进行验证,通过实例验证,满足了计算机联锁系统的安全需求。     

基于项重写系统的联锁系统模型检测方法研究

模型检测方法对安全苛求系统建模的完整性需要一套严谨的方法论与技术,对于验证系统的正确性,具有传统方法无法比拟的优势。提出利用项重写系统建立安全苛求系统模型与验证方法,采用基于项重写系统原理的Maude工具语言,对铁路联锁系统的站场进行形式化建模,通过其语法和语义定义各类约束和离散事件,构架联锁系统属性和行为。在模型建立的基础上,对联锁站场的静态属性和安全属性进行形式化模型验证。结果表明,基于项重写系统的模型检测方法可以较好地应用于实际联锁系统软件的开发,对开发安全苛求系统和模型检测方法的实际应用提供借鉴。     

Testing Formal Specifications to Detect Design Errors

Formal specification and verification techniques are now apused to increase the reliability of software systems. However, these proaches sometimes result in specifying systems that cannot be realized or that are not usable. This paper demonstrates why it is necessary to test specifications early in the software life cycle to guarantee a system that meets its critical requirements and that also provides the desired functionality. Definitions to provide the framework for classifying the validity of a functional requirement with respect to a formal specification tion are also introduced. Finally, the design of two tools for testing formal specifications is discussed.     

A Formal Verification Environment for Railway Signaling System Design

A fundamental problem in the design and development of embedded control systems is the verification of safety requirements. Formal methods, offering a mathematical way to specify and analyze the behavior of a system, together with the related support tools can successfully be applied in the formal proof that a system is safe. However, the complexity of real systems is such that automated tools often fail to formally validate such systems.This paper outlines an experience on formal specification and verification carried out in a pilot project aiming at the validation of a railway computer based interlocking system. Both the specification and the verification phases were carried out in the JACK (Just Another Concurrency Kit) integrated environment. The formal specification of the system was done by means of process algebra terms. The formal verification of the safety requirements was done first by giving a logical specification of such safety requirements, and then by means of model checking algorithms. Abstraction techniques were defined to make the problem of safety requirements validation tractable by the JACK environment.     

Formal probabilistic analysis of a surgical robot control algorithm with different virtual fixtures

Surgical robots are increasingly being used in operation theaters involving normal or laparoscopic surgeries. The working of these surgical robots is highly dependent on their control algorithms, which require very rigorous analysis to ensure their correct functionality due to the safety-critical nature of surgeries. Traditionally, safety of control algorithms is ensured by simulations, but they provide incomplete and approximate analysis results due to their inherent sampling-based nature. We propose to use probabilistic model checking, which is a formal verification method, for quantitative analysis, to verify the control algorithms of surgical robots in this paper. As an illustrative example, the paper provides a formal analysis of a virtual fixture control algorithm, implemented in a neuro-surgical robot, using the PRISM model checker. In particular, we provide a formal discrete-time Markov chain-based model of the given control algorithm and its environment. This formal model is then analyzed for multiple virtual fixtures, like cubic, hexagonal and irregular shapes. This verification allowed us to discover new insights about the considered algorithm that allow us to design safer control algorithms.     

Applying formal verification to the AAMP5 microprocessor: A case study in the industrial use of formal methods

Formal specification combined with mechanical verification is a promising approach for achieving the extremely high levels of assurance required of safety-critical digital systems. However, many questions remain regarding their use in practice: Can these techniques scale up to industrial systems, where are they likely to be useful, and how should industry go about incorporating them into practice? This paper discusses a project undertaken to answer some of these questions, the formal verification of the microcode in the AAMP5 microprocessor. This project consisted of formally specifying in the PVS language a Rockwell proprietary microprocessor at both the instruction-set and register-transfer levels and using the PVS theorem prover to show the microcode correctly implemented the instruction-level specification for a representative subset of instructions. Notable aspects of this project include the use of a formal specification language by practicing hardware and software engineers, the integration of traditional inspections with formal specifications, and the use of a mechanical theorem prover to verify a portion of a commercial, pipelined microprocessor that was not explicitly designed for formal verification.     

Formal methods for verification and validation of partial specifications: A case study

This paper describes our work exploring the suitability of formal specification methods for independent verification and validation (IV&V) of software specifications for large, safety-critical systems. An IV&V contractor often has to perform rapid analysis on incomplete specifications, with no control over how those specifications are represented. Lightweight formal methods show significant promise in this context, as they offer a way of uncovering major errors without the burden of full proofs of correctness. We describe a case study of the use of partial formal models for IV&V of the requirements for Fault Detection Isolation and Recovery on the space station. We conclude that the insights gained from formalizing a specification are valuable, and it is the process of formalization, rather than the end product, that is important. It was only necessary to build enough of the formal model to test the properties in which we were interested. Maintenance of fidelity between multiple representations of the same requirements (as they evolve) is still a problem, and deserves further study.     

基于函数式语义的循环和递归程序结构通用证明技术

各类安全攸关系统的可靠运行离不开软件程序的正确执行.程序的演绎验证技术为程序执行的正确性提供高度保障.程序语言种类繁多,且用途覆盖高可靠性场景的新式语言不断涌现,难以为每种语言设计支撑其程序验证任务的整套逻辑规则,并证明其相对于形式语义的可靠性和完备性.语言无关的程序验证技术提供以程序语言的语义为参数的验证过程及其可靠性结果.对每种程序语言,提供其形式语义后可直接获得面向该语言的程序验证过程.提出一种面向大步操作语义的语言无关演绎验证技术,其核心是对不同语言中循环、递归等可导致无界行为的语法结构进行可靠推理的通用方法.特别地,借助大步操作语义的一种函数式形式化提供表达程序中子结构所执行计算的能力,从而允许借助辅助信息对子结构进行推理.证明所提出验证技术的可靠性和相对完备性,通过命令式、函数式语言中的程序验证实例初步评估了该技术的有效性,并在Coq辅助证明工具中形式化了所有理论结果和验证实例,为基于辅助证明工具实现面向大步语义的语言无关程序验证工具提供了基础.