Teaching formal methods lite via testing

A new style of formal methods course is described, based on a pragmatic approach that emphasizes testing. The course introduces students to formal specification using Z, and shows how formal specification and testing can benefit each other, in both the validation and verification phases. It uses a tools‐based approach, with practical work that reinforces formal specification techniques as well as traditional software engineering skills, such as unit and system testing, inspection and defensive programming with assertions. The two main results are to identify several practical uses of formal specifications that are not widely practised or taught, and to demonstrate that teaching them results in a more interesting and relevant formal methods course. Copyright © 2001 John Wiley & Sons, Ltd.     

Formal Methods in Designing Embedded Systems—the SACRES Experience

From automotive electronics to avionics, embedded systems are part of our everyday life, and developed societies are increasingly dependent on their reliability in operation. At the same time, current design practice is inadequate in coping with the challenge of constructing dependable embedded systems.SACRES is an experimental design environment aimed at the seamless development of embedded systems. It incorporates state-of-the-art industrial design tools and provides formal specification, model checking technology and validated code generation. These concepts have been integrated on the basis of the synchronous approach to reactive systems.As a result, synchronous compilation techniques have been enhanced, in particular as regards techniques for distributed code generation. Formal verification technology was advanced to increase efficiency, handle composed systems and cover some real-time aspects. The new approach of translation validation was developed and proven to work.Real bugs have been found even in well-tested models. It was demonstrated that a formal design including verification is often more efficient than testing. As a consequence, all user partners are committed to further introducing formal design and verification technology.This paper summarises the essential achievements of the project. It explains the results in terms of the basic ideas, the available tools and methodology, as well as the experience gained.     

Application of a Methodology for the Development and Validation of Reliable Process Control Software

This paper discusses the necessity of a good methodology for the development of reliable software, especialy with respect to the final software validation and testing activities. A formal specification development and validation methodology is proposed. This methodology has been applied to the development and validation of a pilot software, incorporating typical features of critical software for nuclear power plant safety protection. The main features of the approach indude the use of a formal specification language and the independent development of two sets of specifications. Analyses on the specifications consists of three-parts: validation against the functional requirements consistency and integrity of the specifications, and dual specification comparison based on a high-level symbolic execution technique. Dual design, implementation, and testing are performed. Automated tools to facilitate the validation and testing activities are developed to support the methodology. These includes the symbolic executor and test data generator/dual program monitor system. The experiences of applying the methodology to the pilot software are discussed, and the impact on the quality of the software is assessed.     

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.     

Combining formal verification and conformance testing for validating reactive systems

This paper presents a combination of verification and conformance testing techniques to support the formal validation of reactive systems. The idea is to use symbolic test selection techniques to extract subgraphs (components) from a specification, and to perform the verification on the components rather than on the whole specification. Under reasonable sufficient conditions, this constitutes a sound compositional verification technique, in the sense that a property verified on the components also holds on the whole specification. This may considerably reduce the global verification effort. Moreover, once verified, a component forms the basis of an adequate test case, i.e. when executed on an implementation, it will not issue false positive or negative verdicts with respect to the verified properties. The approach has been implemented using the STG test selection tool and the PVS theorem prover. It is demonstrated here on a smart‐card application: the Common Electronic Purse System. Copyright © 2003 John Wiley & Sons, Ltd.     

Systematic testing: A means for validating reactive systems

The validity of the first (formal) model of a system to be developed is crucial for the whole development process. Systematically checking this validity helps avoid costs that could arise if it were discovered too late that the system does not satisfy the customer's needs and expectations. This paper addresses how to validate synchronous reactive programs using the technique of systematic testing. Testing reactive systems differs from testing sequential systems: instead of checking simple pairs of inputs and outputs, sequences of inputs and outputs have to be checked. Thus, testing cannot be based on a simple function model, mapping input values onto output values nor on a control flow graph model (where a path from the start node to the final node represents one execution through the represented program). The model widely used instead is that of a finite-state machine. A systematic testing approach is presented that is both effective and efficient for validating reactive systems. It uses an additional specification based on a finite-state machine model. The approach is demonstrated for the well-known lift example. It is shown how to use the specification for carefully choosing a set of test criteria that address different types of fault; a procedure for selecting test cases and test data that satisfy the chosen criteria is presented.     

Hierarchical program specification and verification — a many-sorted logical approach

Summary The notion of abstractions in programming is characterized by the distinction between specification and implementation. As far as the specification structures are concerned, hierarchical program development with abstraction mechanisms is naturally regarded as a process of theory extensions in a many-sorted logic. To support such program development, a language called t is proposed with which one can structuredly build up theories and write their program implementation. There, the implementation is regarded as another level of theory extension, and the relation between the specification and the implementation of an abstraction is characterized in terms of a homomorphism between the two theories. On this formalism, a mechanizable proof method is introduced for validation of implementations of both data and procedural abstraction. Finally, a new data type concept is introduced to generalize the so-called type-parametrization mechanism. A justification of this concept within the first order logic is provided as well as its applications to program structuring and verification.     

Program verification,defeasible reasoning,and two views of computer science

In this paper I attempt to cast the current program verification debate within a more general perspective on the methodologies and goals of computer science. I show, first, how any method involved in demonstrating the correctness of a physically executing computer program, whether by testing or formal verification, involves reasoning that is defeasible in nature. Then, through a delineation of the senses in which programs can be run as tests, I show that the activities of testing and formal verification do not necessarily share the same goals and thus do not always constitute alternatives. The testing of a program is not always intended to demonstrate a program's correctness. Testing may seek to accept or reject nonprograms including algorithms, specifications, and hypotheses regarding phenomena. The relationship between these kinds of testing and formal verification is couched in a more fundamental relationship between two views of computer science, one properly containing the other.     

Verification of external specifications of reactive systems

External specification is currently approached by specification languages for describing and analyzing system requirements. The external specification can be defined during the early stages of the system development and can be very useful for: checking the class/system/subsystem requirements; checking the system composition; evaluating costs of reuse; defining validated reference requirements, histories, and traces for the final validation. The paper presents a collection of criteria in order to formally verify the external specification of reactive systems/subsystems. The verification criteria are grounded on the Tempo Reale object-oriented language (TROL) specification model for real-time systems. In TROL, the external specification is expressed in terms of ports and clauses with temporal constraints. The goal of the verification criteria presented is to check the completeness and consistency of the external specification with special attention to temporal constraints. These criteria can be applied to other real-time specification models and have been enforced in the tool object oriented machine state (TOOMS) tool. A practical example illustrates the verification process that embodies these criteria     

面向RISC-V内存一致性测试的自动化分析方法

开源架构RISC-V定义了其内存一致性模型RVWMO,作为多核RISC-V系统软硬件设计开发的重要规范。在多核芯片的验证阶段,需要对芯片的内存一致性进行严格全面的测试。测试通常针对某一访存顺序模式,选取典型的并行程序片段进行大规模测试（又称Litmus测试）,通过程序运行的最终状态推测芯片内存一致性模型。通常,更为宽松的内存一致性会导致更多的程序状态。分析Litmus测试结果对于验证芯片的RVWMO兼容性、探索多核系统的内存一致性优化的可能性具有重要意义。以RVWMO规范下允许的程序状态为基准,芯片实测得到更多的程序状态表明其存在兼容性问题,得到更少的程序状态表明其仍具有优化空间。面对规模庞大、行为复杂的Litmus测试,如何对其测试结果进行自动化分析是亟待解决的问题。本文对Litmus测试的原理和输出结果进行了深入分析,提出一种面向RISC-V内存一致性测试的自动化分析方法,采用形式化方法对Litmus测试进行基于RVWMO规范的模拟运行,并通过与芯片的实测结果进行对比分析给出测试结论。本方法基于Hifive Unmatched开发板开展测试。实验表明,本文提出的方法可快速、有效地对RISC-V内存一致性测试进行自动化分析。     

实时程序设计方法的发展趋势

本文概述了目前实时程序设计方法学的两个基本方面:实时程序设计语言和实时程序的规范说明及形式化验证。讨论了实时程序设计的基本特点和与一般程序设计的不同之处。程序层次的实时性包括静态的时间限制表达和动态的时间限制维护.程序规范层次的实时性包括建立规范说明模型和形式化证明。     

A service creation environment based on scenarios

Scenarios are often constructed for illustrating example runs through reactive system. Scenarios that describe possible interactions between a system and its environment are widely used in requirement engineering, as a means for users to communicate their functional requirements. Various software development methods use scenarios to define user requirements, but often lack tool support. Existing tools are graphical editors rather than tool support for design. This paper presents a service creation environment for elicitation, integration, verification and validation of scenarios. A semi-formal language is defined for user oriented scenario representation, and a prototype tool implementing an algorithm that integrates them for formal specification generation. This specification is then used to automatically find and report inconsistencies in the scenarios.     

Prospec: Support for Elicitation and Formal Specification of Software Properties

Although formal verification techniques have been demonstrated to improve program dependability, software practitioners have not widely adopted them. One reason often cited is the difficulty in writing formal specifications. This paper introduces Prospec, a tool to assist practitioners in formally specifying software properties. Prospec uses property patterns and scopes. Previous efforts at providing tool support for property specification have not provided convenient abstractions for specifying properties that include multiple events or conditions. A taxonomy of composite propositions is introduced to address this issue by defining relations among propositions and providing graphical abstractions that can assist in specification and validation of properties. This paper shows how composite propositions can enhance the specification pattern system by helping practitioners consider subtleties of behavior in sequences and concurrency through directed questions and visual abstractions. The paper introduces an elicitation and specification process to define patterns, scopes, and composite propositions.     

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     

Slicing communicating automata specifications: polynomial algorithms for model reduction

In the industry, communicating automata specifications are mainly used in fields where the reliability requirements are high, as this formalism allow the use of powerful validation tools. Still, on large scale industrial specifications, formal methods suffer from the combinatorial explosion phenomenon. In our contribution, we suggest to try to bypass this phenomenon, in applying slicing techniques preliminarily to the targeted complex analysis. This analysis can thus be performed a posteriori on a reduced (or sliced) specification, which is potentially less exposed to combinatorial explosion. The slicing method is based on dependence relations, defined on the specification under analysis, and is mainly founded on the literature on compiler construction and program slicing. A theoretical framework is described, for static analyses of communicating automata specifications. This includes formal definitions for the aforementioned dependence relations, and for a slice of a specification with respect to a slicing criterion. Efficient algorithms are also described in detail, for calculating dependence relations and specification slices. Each of these algorithms has been shown to be polynomial, and sound and complete with respect to its respective definition. These algorithms have also been implemented in a slicing tool, named Carver, that has shown to be operational in specification debugging and understanding. The experimental results obtained in model reduction with this tool are promising, notably in the area of formal validation and verification methods, e.g.model checking, test case generation.     

An approach to applying SOFL for agile process and its application in developing a test support tool

Structured Object-Oriented Formal Language (SOFL) is a representative formal engineering method for software development. It offers a three-step specification approach to constructing formal specifications, and specification-based inspection and testing for verification and validation. In this paper, we describe a novel approach to applying the SOFL method to achieve agile development process. This approach results from our experience in several collaboration projects with industry, and aims to strike a balance between the fast delivery of software product and the assurance of its quality. We have tested the approach in developing a prototype test support tool.     

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

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