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

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

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

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

Formal Design of Cache Memory Protocols in IBM

We describe the formal design techniques currently used in IBM to develop cache protocol controllers for high-end servers. In our approach to formal design, formal specification and verification methods are incorporated into the hardware design process, starting from the earliest stages of a hardware project. We describe collaborations between a formal methods expert and hardware designers on two high performance server projects. Properties of the design are verified using both manual proof techniques and model checking. We discuss the modelling and model checking techniques we have developed and indicate future directions.     

Tool-Assisted Specification and Verification of Typed Low-Level Languages

Bytecode verification is one of the key security functions of several architectures for mobile and embedded code, including Java, Java Card, and .NET. Over the past few years, its formal correctness has been studied extensively by academia and industry, using general-purpose theorem provers. The objective of our work is to facilitate such endeavors by providing a dedicated environment for establishing the correctness of bytecode verification within a proof assistant. The environment, called Jakarta, exploits a methodology that casts the correctness of bytecode verification relatively to a defensive virtual machine that performs checks at run-time and to an offensive one that does not; it can be summarized as stating that the two machines coincide on programs that pass bytecode verification. Such a methodology has been used successfully to prove the correctness of the Java Card bytecode verifier and may potentially be applied to many similar problems. One definite advantage of the methodology is that it is amenable to automation. Indeed, Jakarta automates the construction of an offensive virtual machine and a bytecode verifier from a defensive machine, and the proofs of correctness of the bytecode verifier. We illustrate the principles of Jakarta on a simple low-level language extended with subroutines and discuss its usefulness to proving the correctness of the Java Card platform.     

A hardware/software prototyping system for driving assistance investigations

A holistic design and verification environment to investigate driving assistance systems is presented, with an emphasis on system-on-chip architectures for video applications. Starting with an executable specification of a driving assistance application, subsequent transformations are performed across different levels of abstraction until the final implementation is achieved. The hardware/software partitioning is facilitated through the integration of OpenCV and SystemC in the same design environment, as well as OpenCV and Linux in the run-time system. We built a rapid prototyping, FPGA-based camera system, which allows designs to be explored and evaluated in realistic conditions. Using lane departure and the corresponding performance speedup, we show that our platform reduces the design time, while improving the verification efforts.     

脉动阵列的自动综合—FP方法

本文将FP代数,重写理论与脉动阵列(Systolic Arrays)的设计结合起来,研究了脉动阵列的形式化设计和自动综合的问题。文章中提出的FP/B并发计算型,不但可表示某一类FP/B递归方程的展开式解,而且可以用来等价地对算法进行重新描述,从而开发了计算的并行性和流水线性,获得一个规整高效的计算结构。文章形式地用FP/B定义了脉动式,并根据FP/B代数,建立了具有终止性和保持正确性的脉动阵列重写系统,它能将用户FP/B程序自动转换为等价的脉动式,再根据FP/B并发计算型及一些函数的几何语义可较为直接地获得一个脉动阵列的硬件描述。文末给出一个例子加以说明。     

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.     

Overview of software engineering

It is nearly 17 years since the unofficial birth of ‘software engineering’ as a discipline. Mathematics can now be applied to the task of computer programming — turning it into a science. The techniques developed over the period have now matured to an extent where they can be applied in the ‘real world’, rather than just in an academic environment. Mathematics can be used to specify a computer system at a very high level of abstraction, the resultant specification being the computing equivalent of an engineer's blueprint. Such a specification can be used as the basis for developing a computer system, allowing each design decision to be documented and a clear development path charted; thus making maintenance and improvements easier. The exercise of writing a formal specification frequently reveals misconceptions in the minds of both the developer and his customer.Further, the existence of such a specification will allow the verification of the developed software — a mathematical proof of correctness. The development of computer software using formal methods is reviewed, some indication of future trends will be given, and how the ideas of software engineering can be applied today.     

交互式用户界面的形式化描述与性质验证

随着人机交互技术的发展,计算机和用户之间的接口越来越自然,但用户界面管理系统内部的复杂度却大大地增加了.目前提出的新一代用户界面的模型大都停留在概念模型阶段,缺乏对模型的严格描述和证明.该文结合对基于自然交互方式的用户界面的研究成果,归纳出了一个交互式用户界面的通用模型.为了保证系统设计的正确性,文章讨论了如何使用形式化描述语言LOTOS(language of temporal ordering specification)和基于动作的时序逻辑ACTL(action based temporal log     

Verification of Systolic Array:An FP Functional Approach

There has been much interest in the use of formal techniques for the design and analysis ofsystolic arrays.One important aspect of analysis of systolic array is the correctness problem.A few attempts for the verification of systolic array have appeared in the literature.The deficiency is that all of these methods lack a straightforward way of proving correctness.They need either proposing a solution,then applying inductive techniques or showing that thearray satisfies three types of properties:safety,liveness and termination.In this paper,an FP functional approach is proposed.The goal is to verify that a givensystolie design computes the function for which it was intended,lnstead of the generation of asystolic architecture,the method generates a system of recursive functional equations whichdescribes the algorithm executed by the architecture.This representation consists of severalequations describing processes executed by local cells,equations describing connectionsbetween cells,functions representing data streams,and functions describing the relationbetween the structure of input and output data and the systolic array structures.The minimumsolution of the system of recursive functional equations is the function computed by the systolicarchitecture.The main advantage of this approach is that it allows us to develop an algebra offunctional programs. We have developed various methods to deal with different kinds ofsystems of functional recursive equations.By solving the system of recursive functionalequations,we can get the least solution directly.This provides a straightforward way forproving correctness.An example is given.A typical system of recursive functional equations is generated,which can represent most of systolic design.Algebra method is developed showing how to solvethis problem.     

Verification Approach of Metropolis Design Framework for Embedded Systems

In this paper, we focus on the verification approach of Metropolis, an integrated design framework for heterogeneous embedded systems. The verification approach is based on the formal properties specified in Linear Temporal Logic (LTL) or Logic of Constraints (LOC). Designs may be refined due to synthesis or be abstracted for verification. An automatic abstraction propagation algorithm is used to simplify the design for specific properties. A user-defined starting point may also be used with automatic propagation. Two main verification techniques are implemented in Metropolis the formal verification utilizing the model checker Spin and the simulation trace checking with automatic generated checkers. Translation algorithms from specification models to verification models, as well as algorithms of generated checkers are discussed. We use several case studies to demonstrate our approach for verification of system level designs at multiple levels of abstraction.     

BP算法的脉动阵列结构在FPGA上的实现

提出了一种用于实现BP神经网络的串行输入串行输出的脉动阵列结构,在FPGA上实现了基于该阵列结构的用于进行“A－Z” 的印刷体字符识别系统。文中对FPGA中运算部件的微结构进行了讨论。实验结果表明,与软件实现相比用FPGA实现神经网络算法能够极大地提高BP网络的学习和分类速度。     

Top-down design of embedded real-time AI systems

A formal method is proposed for the specification and verification of embedded real-time systems. We consider distributed systems in which parallel processes communicate by sending messages along synchronous or asynchronous channels. To verify that a program satisfies a specification, a compositional proof system is given. Compositionality enables verification during the process of top-down program design. This is illustrated by an example of a rail road crossing. Starting from an assertional specification, we design a program that controls lamps and barriers using information from sensors that signal the passage of trains at a certain distance from the crossing.     

Systolic self-organizing lists under transpose

Systolic array architectures for self-organizing linear lists under the transpose update heuristic are presented. The first model has linear delay and restricts input on every other system cycle. The second system combines a systolic array with trees to provide logarithmic delay and input on every clock cycle. These preliminary designs can be the basis of hardware used to achieve high-speed lossless data compression for data communication and storage. On large files (greater than 40 kilobytes), our designs provide better compression than other systolic list compression schemes     

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.