Efficient Verification of Sequential and Concurrent C Programs

There has been considerable progress in the domain of software verification over the last few years. This advancement has been driven, to a large extent, by the emergence of powerful yet automated abstraction techniques such as predicate abstraction. However, the state-space explosion problem in model checking remains the chief obstacle to the practical verification of real-world distributed systems. Even in the case of purely sequential programs, a crucial requirement to make predicate abstraction effective is to use as few predicates as possible. This is because, in the worst case, the state-space of the abstraction generated (and consequently the time and memory complexity of the abstraction process) is exponential in the number of predicates involved. In addition, for concurrent programs, the number of reachable states could grow exponentially with the number of components. We attempt to address these issues in the context of verifying concurrent (message-passing) C programs against safety specifications. More specifically, we present a fully automated compositional framework which combines two orthogonal abstraction techniques (predicate abstraction for data and action-guided abstraction for events) within a counterexample-guided abstraction refinement scheme. In this way, our algorithm incrementally increases the granularity of the abstractions until the specification is either established or refuted. Additionally, a key feature of our approach is that if a property can be proved to hold or not hold based on a given finite set of predicates $\mathcal{P}$ , the predicate refinement procedure we propose in this article finds automatically a minimal subset of $\mathcal{P}$ that is sufficient for the proof. This, along with our explicit use of compositionality, delays the onset of state-space explosion for as long as possible. We describe our approach in detail, and report on some very encouraging experimental results obtained with our tool MAGIC.     

并发程序验证的时序Petri网方法

并发程序的设计、分析和验证已经成为计算机理论界基础理论研究的方向之一。Petri网和时序逻辑被认 为是探讨该问题较为有效的两个理论工具,但二者都有局限性。该文引用一种新网子类;时序Petri网,描述了并发程序的时序Petri网建模方法;利用网结构描述程序基本框架及保证语句的原子性,通过时序逻辑公式反映程序的共享逻辑变量的赋值变化及时序关系,从而有效地对基本网无法描述的并发程序进行了建模;在此基础上,结合Petri网的可达图分析技术和时序逻辑的演绎公式,分析和验证了并发程序的安全性和活性性质。     

基于分离逻辑的并行程序性质验证方法

随着多核多线程并行执行方式的普及,并行程序形式化验证的需求日显突出.并行程序验证中执行流程的不确定性使验证的内容与目标的关系难以确定,且从并行程序直接进行性质验证会导致验证规模大.为此,提出一种基于分离逻辑的新的验证方法.该方法根据分离逻辑的程序语义描述兼有解释语义和公理语义的特点,从验证的性质出发,把要验证的性质式转换成并行语句序列的逻辑组合式,并进行整理和化简;然后,利用分离逻辑公理系统对语句序列进行验证,用验证了的断言集来求出性质的真值.实例进一步说明,此方法更有效,同时也简化了验证的规模.     

Maximally Concurrent Programs

Typically, program design involves constructing a program P that implements a given specification S; that is, the set ${\overline P}$ of executions of P is a subset of the set ${\overline S}$ of executions satisfying S. In many cases, we seek a program P that not only implements S, but for which ${\overline P}$ = ${\overline S}$. Then, every execution satisfying the specification is a possible execution of the program; we then call P maximal for the specification S. We argue that maximality is an important criterion in the context of designing concurrent programs because it disallows implementations that do not exhibit enough concurrency. In addition, a maximal solution can serve as a basis for deriving a variety of implementations, each appropriate for execution on a specific computing platform. This paper also describes a method for proving the maximality of a program with respect to a given specification. Even though we prove facts about possible executions of programs, there is no need to appeal to branching time logics; we employ a fragment of linear temporal logic for our proofs. The method results in concise proofs of maximality for several non-trivial examples. The method may also serve as a guide in constructing maximal programs. Received September 1997 / Accepted in revised form May 2000     

Properties of Concurrent Programs

A program property is a predicate on programs. In this paper we explore program properties for safety, progress and parallel composition, of the form U ? V where U and V are either predicates on states of a program or program properties, and ? satisfies three rules that are also enjoyed by implication. We show how such properties can be used to reason about concurrent programs. Our motivation is to explore methods of reasoning based on a very small number of widely-known rules.     

量子程序验证

量子硬件设计与制造技术的飞速发展使得人们开始预言大于一百个量子比特的特定用途的量子计算机有望在5-10年内实现.可以想见,到那时候,量子软件的开发将变成真正发挥这些计算机能力的关键.然而,由于量子信息的不可克隆性和纠缠的非局域作用等量子特征,如何设计正确高效的量子程序和量子通信协议将是一个富有挑战性的课题.形式化验证方法,特别是模型检测技术,已经在经典软件设计和系统建模方面被证明行之有效,因此量子软件的形式化验证也开始受到越来越多的关注.本文从量子顺序程序验证和量子通信协议验证两方面,对近年来国内外学者,特别是两位作者所在的研究组在该研究领域取得的一些成果进行了系统的总结.最后,对未来可能的研究方向和面临的挑战进行了简单展望.     

The Evolution of Concurrent Programs

Process algebra are formal languages used for the rigorous specification and analysis of concurrent systems. By using a process algebra as the target language of a genetic programming system, the derivation of concurrent programs satisfying given problem specifications is possible. A genetic programming system based on Koza's model has been implemented. The target language used is Milner's CCS process algebra, and is chosen for its conciseness and simplicity. The genetic programming environment needs a few adaptations to the computational characteristics of concurrent programs. In particular, means for efficiently controlling the exponentially large computation spaces that are common with process algebra must be addressed. Experimental runs of the system successfully evolved a number of non–iterative CCS systems, hence proving the potential of evolutionary approaches to concurrent system development.     

Interface-Based Specification and Verification of Concurrency Controllers

We present a modular approach to specification and verification of concurrency controllers by decoupling their behavior and interface specifications. The behavior specification of a concurrency controller defines how its shared variables change their values whereas the interface specification defines the order in which a client thread should call its methods. We show that the concurrency controllers can be designed modularly by composing their interfaces. We separate the verification of the concurrency controllers from the verification of the threads that use them. For the verification of the concurrency controllers we use infinite state verification techniques which enable us to verify controllers with parameterized constants and arbitrary number of user threads. We automatically generate Java monitors from the concurrency controller specifications which preserve the verified properties. For the thread verification we use finite state program verification tools which enable us to verify Java threads without any restrictions. We show that the user threads can be verified using stubs generated from the concurrency controller interfaces which improves the efficiency of the thread verification significantly.     

Formal Specification and Verification of Distributed Systems

Computations of distributed systems are extremely difficult to specify and verify using traditional techniques because the systems are inherently concurrent, asynchronous, and nondeterministic. Furthermore, computing nodes in a distributed system may be highly independent of each other, and the entire system may lack an accurate global clock.     

一种并发系统的规约方法

提出了并发系统的一种规约方法．这一方法可用于对并发系统进行建模和对模型的验证．将形式化工具融入到一种二维的规约方法中,这样就能使形式化工具更易于应用到并发软件的开发过程中．此外,还提出了一种并发系统的形式化抽象模型．     

Distilling Programs for Verification

In this paper, we show how our program transformation algorithm called distillation can not only be used for the optimisation of programs, but can also be used to facilitate program verification. Using the distillation algorithm, programs are transformed into a specialised form in which functions are tail recursive, and very few intermediate structures are created. We then show how properties of this specialised form of program can be easily verified by the application of inductive proof rules. We therefore argue that the distillation algorithm is an ideal candidate for inclusion within compilers as it facilitates the two goals of program optimization and verification.     

基于规则的用例规约验证方法

用例模型描述了参与者对系统功能的需求,在整个系统的开发过程中有着重要作用;用例描述若存在问题,会对系统开发造成很大影响。提出了一种用例规约的规则验证方法,通过分析用例规约中的错误类别,在特定的用例规约描述方法上设计了帮助发现规约中不完整性、不一致性错误的验证规则,并通过规则的形式化来支持需求的自动化验证。     

基于TLA＋的BRP协议规约及验证

BRP协议是为不可靠信道上传送大数据包文件设计的工业协议。该协议的正确性依赖于各部件实时方面的假设。本文主要阐述了使用时序规约语言TLA＋对BRP协议进行规约和验证的过程。首先通过自然语言非形式化地描述BRP协议的基本原理和需求，在此基础上建立了BRP的形式化模型，利用TLA＋先对不考虑实时要求的BRP进行规约，然后添加实时约束获得BRP完整的规约，最后使用模型检验器TLC验证BRP协议的各种性质。     

Specification and Verification using Message Sequence Charts

Message sequence charts is a notation used in practice by protocol designers and system engineers. In this survey, some of the recent results related to this notation, in the context of specification and automatic verification of communication protocols, are presented.     

Formal Techniques for Protocol Specification and Verification

Certain formal approaches, such as transition techniques and reachability analysis, show promising results when applied to protocol specification and verification.     

基于Z的协议形式描述与验证

一、引言在过去的十年.计算机网络与分布式系统已取得了很大的进展[6j。步入九十年代,各种新型通信技术和分布式应用已相继出现.并已对计算机通信软件发生了重要影响。这些新技术及应用主要包括高速光纤网、多媒体通信、宽带综合业务数字网(B一IsDN)、智能网络技术.如智能服务器、智能路由选择、智能协议开发环境等.以及综合语音、数据、图文和图象服务等等。为了适应这种形势的发展一门新兴的学科一协议工程已应运而生川。     

Linearity Analysis of Concurrent Logic Programs

Automatic memory management and the hiding of the notion of pointers are the prominent features of symbolic processing languages. They make programming easy and guarantee the safety of memory references. For the memory management of linked data structures, copying garbage collection is most widely used because of its simplicity and desirable properties. However, if certain properties about runtime storage allocation and the behavior of pointers can be obtaind by static analysis, a compiler may be able to generate object code closer to that of procedural programs. In the fields of parallel, distributed and real-time computation, it is highly desirable to be able to identify data structures in a program that can be managed without using garbage collection. To this end, this paper proposes a framework of linearity analysis for a concurrent logic language Moded Flat GHC, and proves its basic property. The purpose of linearity analysis is to distinguish between fragments of data structures that may be referenced by two or more pointers and those that cannot be referenced by two or more pointers. Data structures with only one reader are amenable to compile-time garbage collection or local reuse. The proposed framework of linearity analysis is constraint-based and involves both equality and implicational constraints. It has been implemented as part of klint v2, a static analyzer for KL1 programs.     

Dedicative Verification of Reflex Programs

Programming and Computer Software - This paper presents a new two-step verification method for control software. The novelty of the method is that it reduces the verification of the temporal...     

一种基于并发路径的协议验证方法

通信协议验证方法中 ,可达性分析是一种方便的、易于自动化处理的、有效的协议验证方法 .但是随着通信协议的多样性和复杂性的不断增加 ,状态爆炸问题使得可达性分析变得难以实施 .本文采用分而治之的策略 ,提出一种基于并发路径的协议验证方法 .该方法将协议划分为相互独立的并发路径 ,通过逐一分析验证各并发路径 ,来实现验证整个协议的目的 .由于各并发路径的生成和分析都是相互独立的 ,整个协议验证对内存的需求仅受限于各并发路径的复杂度 ,因此有效地缓解了状态爆炸的问题     

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.