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

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

基于时序描述逻辑的UML状态图语义

将UML图形转换成形式化规范是一种精确UML语义、扩大形式化软件方法适用范围的有效途径。鉴于描述逻辑强的可判定推理能力,提出一种采用时序描述逻辑形式化UML状态图,对描述逻辑进行时序扩展,得到可以表示动态和时序语义的形式化规范——时序描述逻辑,给出一套UML状态图向时序描述逻辑表达式转换的规则,通过实例验证了该方法的可行性。     

基于HOL4的形式化方法

针对计算机系统设计的正确性问题,研究了一种在测试空间上完备的形式化方法,探讨了硬件系统在定理证明器HOL4中进行形式化验证的一般方法,其中包括如何采用高阶逻辑形式化描述系统的实现与规范,以及在HOL4中证明目标的一般过程.同时,以乘法器为实例,提出一种功能分解法对需要分析的电路进行形式化建模,并对模型的性质在HOL4中进行推理与验证,从而证明了乘法器电路设计的模型满足所提取的性质.     

形式化方法概貌

形式化方法是基于严格数学基础,对计算机硬件和软件系统进行描述、开发和验证的技术.其数学基础建立在形式语言、语义和推理证明三位一体的形式逻辑系统之上.形式化方法已经以不同程度和不同方式愈来愈多地应用在计算系统生命周期的各个阶段.介绍了形式化方法的发展历程和基本方法体系;以形式规约和形式验证为主线,综述了形式化方法的理论、方法、工具和应用的现状,展示了形式化方法与软件学科其他领域的交叉和融合;分析了形式化方法的启示,并展望了其面临的发展机遇和未来趋势.形式化方法的发展和研究现状表明：其应用已经取得了长足的进步,在提高计算系统的可靠性和安全性方面发挥了重要作用.在当今软件日益成为社会基础设施的时代,形式化方法将与人工智能、网络空间安全、量子计算、生物计算等领域和方向交叉融合,得到更加广阔的应用.研究和建立这种交叉融合的理论和方法不仅重要,而且具有挑战性.     

基于Coq的微内核操作系统程序验证方法研究

机载嵌入式程序的可信属性验证是新一代飞机研制最关注的软件质量保障问题;基于定理证明的程序形式化验证方法是一种可靠和严格的软件正确性验证技术;文中在深入分析微内核操作系统的基础上,应用霍尔逻辑针对机载嵌入式软件核心代码开展程序验证技术研究,根据霍尔逻辑的相关推理规则进行程序验证,并在定理证明辅助工具Coq中形式化表示霍尔逻辑的推理规则,针对机载操作系统的部分程序代码实例进行验证;实验结果表明基于定理证明的程序验证方法可以对软件程序代码的正确性进行验证,从而帮助软件提供商开发高可信的机载嵌入式软件。     

软件需求的形式化转换模型

需求规范错误是软件设计错误的一大类。该文提出了一个软件需求的形式化转换模型，用来将软件需求分析直接、自动地转换为形式化描述，为需求验证提供帮助，避免软件在需求规范上可能产生的错误。     

一种基于描述逻辑的UML模型验证方法

针对UML模型中可能会存在的概念不一致、概念冗余等语义一致性问题,该文提出一种基于描述逻辑的UML模型形式化与模型验证方法。该方法首先采用描述逻辑的子系统SHOIN（D）形式化描述UML类图、状态图以及活动图的基本模型构造,进而将UML模型转换为相应的描述逻辑本体,最终借助现有的本体推理机制验证UML模型的语义一致性问题。该方法可以为下一代的软件CASE工具实现软件模型自动推理和验证提供一种可选的技术方案。     

基于Coq的软件安全性验证

针对数组越界、空指针应用和缓冲区溢出三类威胁软件安全的不规范操作,提出了一种基于Coq验证上述三类操作的形式化方法。首先编写三类安全问题的程序实例,并采用形式化方法进行标注;其次运用Frama-C和Why工具对标注程序进行解析,生成需要证明的定理;最后基于Coq集成开发环境证明定理,实现安全问题的验证。结果表明,该方法有效验证了软件安全中的三类问题,为形式化方法在软件安全性验证方面的应用奠定了基础。     

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

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

UML模型到COOZ规约的形式化转换

为UML建模元素提供坚实的形式化语义基础是目前的研究热点之一,在这方面也有了不少探索。文章在过去的研究的基础上,给出了UML模型到COOZ规约的一种系统的转化方法。将UML模型转换到COOZ规约后,UML模型的推理验证就可以通过相应COOZ规约的推理验证实现。该方法不但为UML提供了精确的形式化语义基础,而且,提供了一种UML模型推理的合理的机制。     

基于Object—Z的形式化验证方法

定理证明是一种形式化验证技术，也是形式化方法的重要组成部分，它能从形式规格说明中推理出应具备的性质与属性，从而可以对规格说明进行形式验证。Obiect-Z是形式规格说明语言Z的面向对象扩充，基于集合论与数理逻辑，具有严密的逻辑性，适合精确地描述大型软件系统，并且可以对其形式规格说明进行推理。本文首先给出了基于Object—Z规格说明的定理证明验证方法，接着用Object-Z描述了一个电梯操作系统的实例，在此基础上给出了其形式规格说明的定理证明方法来进行形式化验证。     

带OCL约束条件的类图到object—Z规格说明的转换

如何提高软件的可靠性是目前软件研究领域的一个热点。将形式化方法和主流的软件开发方法相结合是一个可行的方法。本文研究UML语言和Object-Z语言相结合的方法，为主流的软件开发人员所使用的图形化规格说明技术与形式方法提供的精确的分析和验证技术架起了一座桥梁。本文定义如何将带0CL约束条件的类图转换到Object-Z规格说明的方法。这样不仅可以通过支持Object-Z语言的工具采对UML语言描述的系统性质进行验证和确认，而且能够帮助规格说明人员方便地构造Object-Z规格说明。     

面向访问验证保护级的安全VMM形式化原型系统设计和实现

操作系统是计算机软件系统的基础,具有控制逻辑复杂、安全性和可靠性要求高等特点。在国内外高等级安全操作系统的规范和标准中,都提出了对内核进行形式化规范和验证的要求。近年来国内相关研究机构相继开发了满足GB 17859-1999“强制访问控制级”和“结构化保护级”的安全操作系统原型,但对更高级别的安全操作系统的研发尚属空白。在“面向访问验证保护级安全操作系统”课题的研究中,设计并实现了一个基于Haskell的安全VMM原型系统—CASVisor.CASVisor严格定义了系统的形式化规范,可用于指导高性能的C程序的实现,并为形式化的分析和验证打下基础,同时CASVisor具备模拟功能,以便实施基于快速原型的开发方法。     

一个Object-Z规格说明的证明责任产生器

定理证明是一种形式化验证技术,也是形式化方法的重要组成部分,它能从形式规格说明中推理出应具备的性质与属性,从而可以对规格说明进行形式验证。Object-Z是形式规格说明语言Z的面向对象扩充,基于集合论与数理逻辑,具有严密的逻辑性,适合于精确地描述大型软件系统,并且可以对其形式规格说明进行推理。设计一个证明责任产生器,从Object-Z形式规格说明出发,按照相关规则自动抽取相应的证明责任,这些证明责任可以直接输入到已有的定理证明器Z/EVES中进行证明之。证明责任产生器起着Object-Z规格说明编辑器与证明器Z/EVES之间的桥梁作用,方便于Object-Z形式规格说明的验证。     

Hardware-software codesign of embedded systems

Designers generally implement embedded controllers for reactive real-time applications as mixed software-hardware systems. In our formal methodology for specifying, modeling, automatically synthesizing, and verifying such systems, design takes place within a unified framework that prejudices neither hardware nor software implementation. After interactive partitioning, this approach automatically synthesizes the entire design, including hardware-software interfaces. Maintaining a finite-state machine model throughout, it preserves the formal properties of the design. It also allows verification of both specification and implementation, as well as the use of specification refinement through formal verification     

Experiences with software specification and verification using LP,the Larch proof assistant

We sketch a method for deduction-oriented software and system development. The method incorporates formal machine-supported specification and verification as activities in software and systems development. We describe experiences in applying this method. These experiences have been gained by using the LP, the Larch proof assistant, as a tool for a number of small and medium size case studies for the formal development of software and systems. LP is used for the verification of the development steps. These case studies include

? quicksort

? the majority vote problem

? code generation by a compiler and its correctness

? an interactive queue and its refinement into a network.

The developments range over levels of requirement specifications, designs and abstract implementations. The main issues are questions of a development method and how to make good use of a formal tool like LP in a goal-directed way within the development. We further discuss the value of advanced specification techniques, most of which are deliberately not supported by LP and its notation, and their significance in development, Furthermore, we discuss issues of enhancement of a support system like LP and the value and the practicability of using formal techniques such as specification and verification in the development process in practice.     

Analog property checkers: a DDR2 case study

The formal specification component of verification can be exported to simulation through the idea of property checkers. The essence of this approach is the automatic construction of an observer from the specification in the form of a program that can be interfaced with a simulator and alert the user if the property is violated by a simulation trace. Although not complete, this lighter approach to formal verification has been effectively used in software and digital hardware to detect errors. Recently, the idea of property checkers has been extended to analog and mixed-signal systems.     

The KeY tool

KeY is a tool that provides facilities for formal specification and verification of programs within a commercial platform for UML based software development. Using the KeY tool, formal methods and object-oriented development techniques are applied in an integrated manner. Formal specification is performed using the Object Constraint Language (OCL), which is part of the UML standard. KeY provides support for the authoring and formal analysis of OCL constraints. The target language of KeY based development is Java Card DL, a proper subset of Java for smart card applications and embedded systems. KeY uses a dynamic logic for Java Card DL to express proof obligations, and provides a state-of-the-art theorem prover for interactive and automated verification. Apart from its integration into UML based software development, a characteristic feature of KeY is that formal specification and verification can be introduced incrementally.     

Rule-based systems formalized within a software architectural style

This article considers the utilization of architectural styles in the formal design of knowledge-based systems. The formal model of a style is an approach to systems modeling that allows software developers to understand and prove properties about the system design in terms of its components, connectors, configurations, and constraints. This allows commonality of design to be easily understood and captured, leading to a better understanding of the role that an architectural abstraction would have in another complex system, embedded context, or system integration. In this article, a formal rule-based architectural style is presented in detail using the Z notation. The benefits of depicting the rule-based system as an architectural style include reusability, understandability, and the allowance for formal software analysis and integration techniques. The ability to define the rule-based architectural style in this way, illustrates the power, clarity, and flexibility of this specification form over traditional formal specification approaches. In addition, it extends current verification approaches for knowledge-based systems beyond the knowledge base only.     

基于企业流程的需求形式化验证技术

需求验证是为了确保需求规格说明具有良好特性(完整性、一致性、无二义性)而对需求规格说明进行的一种审查活动。目前广泛使用的需求验证技术存在着两个问题:难以处理大型、复杂的需求文档;审查过程需要相当长的时间。该文所研究的基于企业流程的需求形式化验证技术,通过对需求文档中企业流程各活动之间的逻辑关系进行验证,从而发现其中的不一致性和二义性。