Formal verification of Ada programs

The Penelope verification editor and its formal basis are described. Penelope is a prototype system for the interactive development and verification of programs that are written in a rich subset of sequential Ada. Because it generates verification conditions incrementally, Penelope can be used to develop a program and its correctness proof in concert. If an already-verified program is modified, one can attempt to prove the modified version by replaying and modifying the original sequence of proof steps. Verification conditions are generated by predicate transformers whose logical soundness can be proven by establishing a precise formal connection between predicate transformation and denotational definitions in the style of continuation semantics. Penelope's specification language, Larch/Ada, belongs to the family of Larch interface languages. It scales up properly, in the sense that one can demonstrate the soundness of decomposing an implementation hierarchically and reasoning locally about the implementation of each node in the hierarchy     

Formal verification of a pipelined microprocessor

The application of modern functional languages and supporting verification technology to a scaled-down but realistic microprocessor is described. The model is of an infinite stream of machine instructions consuming an infinite stream of interrupt signals and is specified at two levels: instruction and hardware design. A correctness criterion is stated for an appropriate sense of equivalent behavior of these levels and proved using a mechanically supported induction argument. The functional-language-based verification system Clio and the Mini Cayuga microprocessor are described. The formal specification and verification process are examined in detail     

Formal verification of mobile robot protocols

Mobile robot networks emerged in the past few years as a promising distributed computing model. Existing work in the literature typically ensures the correctness of mobile robot protocols via ad hoc handwritten proofs, which, in the case of asynchronous execution models, are both cumbersome and error-prone. Our contribution is twofold. We first propose a formal model to describe mobile robot protocols operating in a discrete space i.e., with a finite set of possible robot positions, under synchrony and asynchrony assumptions. We translate this formal model into the DVE language, which is the input format of the model-checkers DiVinE and ITS tools, and formally prove the equivalence of the two models. We then verify several instances of two existing protocols for variants of the ring exploration in an asynchronous setting: exploration with stop and perpetual exclusive exploration. For the first protocol we refine the correctness bounds and for the second one, we exhibit a counter-example. This protocol is then modified and we establish the correctness of the new version with an inductive proof.     

Formal verification of conflict detection algorithms

Safety assessment of new air traffic management systems is a main issue for civil aviation authorities. Standard techniques such as testing and simulation have serious limitations in new systems that are significantly more autonomous than the older ones. In this paper, we present an innovative approach for establishing the correctness of conflict detection systems. Fundamental to our approach is the concept of trajectory, and how we represent a continuous physical trajectory by a continuous path in the x-y plane constrained by physical laws and operational requirements. From the model of trajectories, we extract, and formally prove, high-level properties that can serve as a framework to analyze conflict scenarios. We use the AILS (Airborne Information for Lateral Spacing) alerting algorithm as a case study of our approach. Published online: 19 November 2002     

The effect of distractor modality and processing code on human-automation interaction

We examined the effect of distractor characteristics (modality and processing code) on visual search performance and interaction with an automated decision aid. Multiple Resource Theory suggests that concurrent tasks that are processed similarly (e.g. two visual tasks) will cause greater interference than tasks that are not (e.g., a visual and auditory task). The impact of tasks that share processing and perceptual demands and their interaction with human-automation interaction is not established. In order to examine this, participants completed two blocks of a luggage screening simulation with or without the assistance of an automated aid. For one block, participants performed a concurrent distractor task drawn from one of four combinations of modality and processing code: auditory-verbal; auditory-spatial; visual-verbal; visual-spatial. We measured sensitivity, criterion setting, perceived workload, system trust, perceived system reliability, compliance, reliance, and confidence. Participants demonstrated highest sensitivity when performing with an auditory-spatial secondary task. Automation compliance was higher when the auditory-spatial distraction was present versus absent; however, system trust was highest in the auditory-verbal condition. Confidence (when disagreeing with the aid) was also highest when the distractor was auditory. This study indicates that some forms of auditory ‘distractors’ may actually help performance; these results further contribute to understanding how distractions influence performance when operators interact with automation and have implications for improved work environment and system design.     

Formal verification of algorithms for critical systems

The authors describe their experience with formal, machine-checked verification of algorithms for critical applications, concentrating on a Byzantine fault-tolerant algorithm for synchronizing the clocks in the replicated computers of a digital flight control system. The problems encountered in unsynchronized systems and the necessity, and criticality, of fault-tolerant synchronization are described. An overview of one such algorithm and of the arguments for its correctness are given. A verification of the algorithm performed using the authors' EHDM system for formal specification and verification is described. The errors found in the published analysis of the algorithm and benefits derived from the verification are indicated. Based on their experience, the authors derive some key requirements for a formal specification and verification system adequate to the task of verifying algorithms of the type considered. The conclusions regarding the benefits of formal verification in this domain and the capabilities required of verification systems in order to realize those benefits are summarized     

Formal verification of a pervasive messaging system

As ubiquitous computing becomes a reality, its applications are increasingly being used in business-critical, mission-critical and even in safety-critical, areas. Such systems must demonstrate an assured level of correctness. One approach to the exhaustive analysis of the behaviour of systems is formal verification, whereby each important requirement is logically assessed against all possible system behaviours. While formal verification is often used in safety analysis, it has rarely been used in the analysis of deployed pervasive applications. Without such formality it is difficult to establish that the system will exhibit the correct behaviours in response to its inputs and environment. In this paper, we show how model-checking techniques can be applied to analyse the probabilistic behaviour of pervasive systems. As a case study we apply this technique to an existing pervasive message-forwarding system, Scatterbox. Scatterbox incorporates many typical characteristics of pervasive systems, such as dependence on sensor reliability and dependence on context. We assess the dynamic temporal behaviour of the system, including the analysis of probabilistic elements, allowing us to verify formal requirements even in the presence of uncertainty in sensors. We also draw some tentative conclusions concerning the use of formal verification for pervasive computing in general.     

Formal hardware verification methods: A survey

Growing advances in VLSI technology have led to an increased level of complexity in current hardware systems. Late detection of design errors typically results in higher costs due to the associated time delay as well as loss of production. Thus it is important that hardware designs be free of errors. Formal verification has become an increasingly important technique towards establishing the correctness of hardware designs. In this article we survey the research that has been done in this area, with an emphasis on more recent trends. We present a classification framework for the various methods, based on the forms of the specification, the implementation, and the proff method. This framework enables us to better highlight the relationships and interactions between seemingly different approaches.     

UML状态机模型形式化验证技术研究

系统建模是系统开发经常用到的分析设计方法,如何保证模型的正确性一直是人们关注的话题.为了验证系统设计的模型正确性,进而提高整个系统的质量,提出了一种通过模型检查技术对UML状态机模型进行动态语义验证的方法.对状态机模型进行形式化描述,根据定义的映射规则将图形信息映射成模型检查器可以读取的语言,分析待验证的性质内容,通过使用模型检查器得到验证结果.     

Formal verification of the NASA runway safety monitor

The runway safety monitor (RSM) designed by Lockheed Martin is part of NASA’s effort to reduce aviation accidents. We developed a Petri net model of the RSM protocol and used the model checking functions of our tool (stochastic and model checking analyzer for reliability and timing) SMART (Stochestic and model checking analyses for seliability and tunnig) to investigate a number of safety properties for the RSM. To mitigate the impact of state-space explosion, we built a highly discretized model of the system, obtained by partitioning the monitored runway zone into a grid of smaller volumes and by considering scenarios involving only two aircraft. The model also assumes that there are no communication failures, such as bad input from radar or lack of incoming data, thus it relies on a consistent view of reality by all participants. In spite of these simplifications, we were able to expose potential problems in the conceptual design of RSM. Our findings were forwarded to the design engineers, who undertook corrective action. Additionally, the results stress the efficiency attained by the new model checking algorithms implemented in SMART, and demonstrate their applicability to real-world systems. Attempts to verify RSM with similar NuSMV and SPIN models have failed due to excessive memory consumption. Work supported in part by the National Aeronautics and Space Administration under grant NAG-1-02095 and by the National Science Foundation under grants CCR-0219745 and ACI-0203971.     

Formal verification of concurrent programs with read-write locks

Read-write locking is an important mechanism to improve concurrent granularity, but it is difficult to reason about the safety of concurrent programs with read-write locks. Concurrent separation logic (CSL) provides a simple but powerful technique for locally reasoning about concurrent programs with mutual exclusive locks. Unfortunately, CSL cannot be directly applied to reasoning about concurrent programs with read-write locks due to the different concurrent control mechanisms. This paper focuses on extending CSL and presenting a proof-carrying code (PCC) system for reasoning about concurrent programs with read-write locks. We extend the heap model with a writing permission set, denoted as logical heap, then define “strong separation” and “weak separation” over logical heap. Following CSL’s local-reasoning idea, we develop a novel program logic to enforce weak separations of heap between different threads and provide verification of concurrent programs with read-write locks.     

Formal verification by symbolic evaluation of partially-ordered trajectories

Symbolic trajectory evaluation provides a means to formally verify properties of a sequential system by a modified form of symbolic simulation. The desired system properties are expressed in a notation combining Boolean expressions and the temporal logic next-time operator. In its simplest form, each property is expressed as an assertion [AC], where the antecedentA expresses some assumed conditions on the system state over a bounded time period, and the consequentC expresses conditions that should result. A generalization allows simple invariants to be established and proven automatically.The verifier operates on system models in which the state space is ordered by information content. By suitable restrictions to the specification notation, we guarantee that for every trajectory formula, there is a unique weakest state trajectory that satisfies it. Therefore, we can verify an assertion [AC] by simulating the system over the weakest trajectory forA and testing adherence toC. Also, establishing invariants correspond to simple fixed point calculations.This paper presents the general theory underlying symbolic trajectory evaluation. It also illustrates the application of the theory to the taks of verifying switch-level circuits as well as more abstract implementations.This research was supported by the Defense Advanced Research Projects Agency, ARPA Order Number 4976, by the National Science Foundation, under grant number MIP-8913667, by operating grant OGPO 109688 from the Natural Sciences and Engineering Research Council of Canada, and by a fellowship from the British Columbia Advanced Systems Institute.     

改进身份认证协议的形式化描述与验证

以前用着色Petri网验证协议,大多只验证了其正确性,采用着色Petri网对自行设计的基于PKI的动态身份认证系统的安全性进行了描述和验证;一般在使用传统1-可达性分析方法分析复杂身份认证协议时,会存在状态空间爆炸的问题,为了有效地解决该问题,提出了一种用1-可迭性分析方法和向回分析方法相结合的策略,对该身份认证协议进行了分析,从而验证了该身份认证协议是安全的.     

Formal verification of behaviour networks including sensor failures

The paper deals with the problem of verifying behaviour-based control systems. Although failures in sensor hardware and software can have strong influences on the robot’s operation, they are often neglected in the verification process. Instead, perfect sensing is assumed. Therefore, this paper provides an approach for modelling the sensor chain in a formal way and connecting it to the formal model of the control system. The resulting model can be verified using model checking techniques, which is shown on the examples of the control systems of an autonomous indoor robot and an autonomous off-road robot.     

Formal verification of neural agents in non-deterministic environments

Autonomous Agents and Multi-Agent Systems - Approval-based multiwinner voting rules have recently received much attention in the Computational Social Choice literature. Such rules aggregate...     

FFT处理机的形式化模型及正确性验证

快速傅立叶变换的应用领域非常广泛,其硬件实现方法多种多样,验证这些电路的正确性具有很强的实用价值。传统的电路正确性验证的方法是模拟,这种方法的主要缺点是随着参与运算的点数的增加,穷尽模拟全部输入情况所耗费的时间越来越长,甚至难以实现。而形式化方法使用纯数学手段证明电路的正确性,克服了传统方法的缺点。首先用重写系统给出了任意N=2M点的基2的流水式快速傅里叶变换处理机的形式化模型,然后给出它的正确性验证,探索了验证处理复数的复杂电路正确性的方法。