UML模型中并发对象的组合验证

本文在用层次自动机结构化表示UML Statecharts的基础上,定义了UML协同图中并发对象的同步合成,然后根据结构间的模拟关系,研究了对并发对象系统进行组合验证的方法和规则,使有可能在对UML协同图进行模型检验的过程中不必建立系统的全局状态图,以缓解状态爆炸问题。     

Automatic symbolic compositional verification by learning assumptions

Compositional reasoning aims to improve scalability of verification tools by reducing the original verification task into subproblems. The simplification is typically based on assume-guarantee reasoning principles, and requires user guidance to identify appropriate assumptions for components. In this paper, we propose a fully automated approach to compositional reasoning that consists of automated decomposition using a hypergraph partitioning algorithm for balanced clustering of variables, and discovering assumptions using the L ^* algorithm for active learning of regular languages. We present a symbolic implementation of the learning algorithm, and incorporate it in the model checker NuSmv. In some cases, our experiments demonstrate significant savings in the computational requirements of symbolic model checking. This research was partially supported by ARO grant DAAD19-01-1-0473, and NSF grants ITR/SY 0121431 and CCR0306382.     

基于抽象-验证-细化范例的软件模型检测

如何保证软件系统的正确性和可靠性是当前软件开发面临的主要问题之一。模型检测作为一种重要的自动化验证技术在软件的分析与验证中正取得越来越多的成功。本文以微软的SLAM和加州大学伯克利分校的BLAST为例综述性地介绍了基于抽象-验证-细化范例的软件模型检测。     

Learning to divide and conquer: applying the L* algorithm to automate assume-guarantee reasoning

Assume-guarantee reasoning enables a “divide-and-conquer” approach to the verification of large systems that checks system components separately while using assumptions about each component’s environment. Developing appropriate assumptions used to be a difficult and manual process. Over the past five years, we have developed a framework for performing assume-guarantee verification of systems in an incremental and fully automated fashion. The framework uses an off-the-shelf learning algorithm to compute the assumptions. The assumptions are initially approximate and become more precise by means of counterexamples obtained by model checking components separately. The framework supports different assume-guarantee rules, both symmetric and asymmetric. Moreover, we have recently introduced alphabet refinement, which extends the assumption learning process to also infer assumption alphabets. This refinement technique starts with assumption alphabets that are a subset of the minimal interface between a component and its environment, and adds actions to it as necessary until a given property is shown to hold or to be violated in the system. We have applied the learning framework to a number of case studies that show that compositional verification by learning assumptions can be significantly more scalable than non-compositional verification. J.M. Cobleigh currently employed by The MathWorks, Inc., 3 Apple Hill Drive, Natick, MA 01760, USA.     

面向源代码的软件模型检测及其实现

模型检测应用于检测软件可靠性具有重要意义.介绍了一种基于谓词抽象和反例引导抽象求精技术对源程序进行建模和验证的模型检测方法,并结合自行研发的Jchecker工具详细介绍了该软件模型检测技术的运作过程和关键算法.     

基于假设保证的SpaceWire总线链路接口的组合验证

SpaceWire是一种面向航天应用的高速、全双工的串行总线标准,对其功能正确性的实现具有极高需求。运用模型检验的方法对SST项目中SpaceWire总线链路接口的设计实现与标准规范的一致性进行形式化的验证。在对SpaceWire总线链路接口进行形式建模时,运用假设保证推理,通过抽象环境状态机,建立层次化的组合验证模型,实现了关键功能属性的验证,并有效地解决了状态爆炸问题,缩短验证时间。该方法克服了模拟和测试等传统验证方法的不完备性,为验证SpaceWire总线链路接口设计与实现的功能正确性提供了有效的验证手段。     

Concurrent software verification with states, events, and deadlocks

We present a framework for model checking concurrent software systems which incorporates both states and events. Contrary to other state/event approaches, our work also integrates two powerful verification techniques, counterexample-guided abstraction refinement and compositional reasoning. Our specification language is a state/event extension of linear temporal logic, and allows us to express many properties of software in a concise and intuitive manner. We show how standard automata-theoretic LTL model checking algorithms can be ported to our framework at no extra cost, enabling us to directly benefit from the large body of research on efficient LTL verification. We also present an algorithm to detect deadlocks in concurrent message-passing programs. Deadlock- freedom is not only an important and desirable property in its own right, but is also a prerequisite for the soundness of our model checking algorithm. Even though deadlock is inherently non-compositional and is not preserved by classical abstractions, our iterative algorithm employs both (non-standard) abstractions and compositional reasoning to alleviate the state-space explosion problem. The resulting framework differs in key respects from other instances of the counterexample-guided abstraction refinement paradigm found in the literature. We have implemented this work in the magic verification tool for concurrent C programs and performed tests on a broad set of benchmarks. Our experiments show that this new approach not only eases the writing of specifications, but also yields important gains both in space and in time during verification. In certain cases, we even encountered specifications that could not be verified using traditional pure event-based or state-based approaches, but became tractable within our state/event framework. We also recorded substantial reductions in time and memory consumption when performing deadlock-freedom checks with our new abstractions. Finally, we report two bugs (including a deadlock) in the source code of Micro-C/OS versions 2.0 and 2.7, which we discovered during our experiments. This research was sponsored by the National Science Foundation (NSF) under grants no. CCR-9803774 and CCR-0121547, the Office of Naval Research (ONR) and the Naval Research Laboratory (NRL) under contract no. N00014-01-1-0796, the Army Research Office (ARO) under contract no. DAAD19-01-1-0485, and was conducted as part of the Predictable Assembly from Certifiable Components (PACC) project at the Software Engineering Institute (SEI). This article combines and builds upon the papers (CCO⁺04) and (CCOS04). Received December 2004 Revised July 2005 Accepted July 2005 by Eerke A. Boiten, John Derrick, Graeme Smith and Ian Hayes     

The software model checker Blast

Blast is an automatic verification tool for checking temporal safety properties of C programs. Given a C program and a temporal safety property, Blast either statically proves that the program satisfies the safety property, or provides an execution path that exhibits a violation of the property (or, since the problem is undecidable, does not terminate). Blast constructs, explores, and refines abstractions of the program state space based on lazy predicate abstraction and interpolation-based predicate discovery. This paper gives an introduction to Blast and demonstrates, through two case studies, how it can be applied to program verification and test-case generation. In the first case study, we use Blast to statically prove memory safety for C programs. We use CCured, a type-based memory-safety analyzer, to annotate a program with run-time assertions that check for safe memory operations. Then, we use Blast to remove as many of the run-time checks as possible (by proving that these checks never fail), and to generate execution scenarios that violate the assertions for the remaining run-time checks. In our second case study, we use Blast to automatically generate test suites that guarantee full coverage with respect to a given predicate. Given a C program and a target predicate p, Blast determines the program locations q for which there exists a program execution that reaches q with p true, and automatically generates a set of test vectors that cause such executions. Our experiments show that Blast can provide automated, precise, and scalable analysis for C programs.     

Formal verification of software source code through semi-automatic modeling

We describe the experience of modeling and formally verifying a software cache algorithm using the model checker RuleBase. Contrary to prevailing wisdom, we used a highly detailed model created directly from the C code itself, rather than a high-level abstract model.     

Automatic software model checking via constraint logic

This paper proposes the use of constraint logic to perform model checking of imperative, infinite-state programs. We present a semantics-preserving translation from an imperative language with recursive procedures and heap-allocated mutable data structures into constraint logic. The constraint logic formulation provides a clean way to reason about the behavior and correctness of the original program. In addition, it enables the use of existing constraint logic implementations to perform bounded software model checking, using a combination of symbolic reasoning and explicit path exploration.     

The formal-CAFE methodology and model checking patterns in the specification of e-commerce systems

Electronic commerce is an important application that has evolved significantly recently. However, electronic commerce systems are complex and difficult to be correctly designed. Guaranteeing the correctness of an e-commerce system is not an easy task due to the great amount of scenarios where errors occur, many of them very subtle. In this work we presents a methodology that uses formal-method techniques, specifically symbolic model checking, to design electronic commerce applications and to automatically verify them. Also, a model checking pattern hierarchy has been developed—it specifies patterns to construct and verify the formal model of e-commerce systems. We consider this research the first step to the development of a framework, which will integrate the methodology, an e-commerce specification language based on business rules, and a model checker. Adriano Pereira received the B.S. and M.S. degrees in computer science in 2000 and 2002, respectively, and he is currently pursuing the Ph.D. degree in computer science from the Federal University of Minas Gerais, Belo Horizonte, Brazil. His current interests are on performance analysis and modeling of e-business and distributed systems, and formal methods. Mark Song received the B.S., M.S. and Ph.D. degrees in computer science from the Federal University of Minas Gerais, Belo Horizonte, Brazil. His current interests are on distributed systems and formal methods – especially BMC (Bounded Model Checking). Gustavo Franco received the B.S. and M.S. degrees in computer science in 2001 and 2004, respectively, from the Federal University of Minas Gerais, Belo Horizonte, Brazil. His research was on modeling the user behavior of e-business and distributed systems, and formal methods. Actually his current interests are on software engeneering and project management of IT projects.     

Automated assumption generation for compositional verification

We describe a method for computing a minimum-state automaton to act as an intermediate assertion in assume-guarantee reasoning, using a sampling approach and a Boolean satisfiability solver. For a set of synthetic benchmarks intended to mimic common situations in hardware verification, this is shown to be significantly more effective than earlier approximate methods based on Angluin’s L* algorithm. For many of these benchmarks, this method also outperforms BDD-based model checking and interpolation-based model checking. We also demonstrate how domain knowledge can be incorporated into our algorithm to improve its performance.     

A classification and comparison of model checking software architecture techniques

Software architecture specifications are used for many different purposes, such as documenting architectural decisions, predicting architectural qualities before the system is implemented, and guiding the design and coding process. In these contexts, assessing the architectural model as early as possible becomes a relevant challenge. Various analysis techniques have been proposed for testing, model checking, and evaluating performance based on architectural models. Among them, model checking is an exhaustive and automatic verification technique, used to verify whether an architectural specification conforms to expected properties. While model checking is being extensively applied to software architectures, little work has been done to comprehensively enumerate and classify these different techniques.The goal of this paper is to investigate the state-of-the-art in model checking software architectures. For this purpose, we first define the main activities in a model checking software architecture process. Then, we define a classification and comparison framework and compare model checking software architecture techniques according to it.     

单道批处理系统的建模与验证

单道批处理系统的模型是其性能评价、仿真、作业调度及控制的研究基础。建立了单道批处理系统的一个数学模型—批处理自动机,并给出了相应的转换算法,将所建数学模型转换成Kripke结构;完成了基于Kripke结构的单道批处理系统模型检测,验证了单道批处理系统的合理性即兼顾公平性与效率。     

Counterexample-guided predicate abstraction of hybrid systems

Predicate abstraction has emerged to be a powerful technique for extracting finite-state models from infinite-state systems, and has been recently shown to enhance the effectiveness of the reachability computation techniques for hybrid systems. Given a hybrid system with linear dynamics and a set of linear predicates, the verifier performs an on-the-fly search of the finite discrete quotient whose states correspond to the truth assignments to the input predicates. The success of this approach depends on the choice of the predicates used for abstraction. In this paper, we focus on identifying these predicates automatically by analyzing spurious counterexamples generated by the search in the abstract state-space. We present the basic techniques for discovering new predicates that will rule out closely related spurious counterexamples, optimizations of these techniques, implementation of these in the verification tool, and case studies demonstrating the promise of the approach.     

Compositional Verification of Knowledge-Based Task Models and Problem-Solving Methods

In this paper a compositional verification method for task models and problem-solving methods for knowledge-based systems is introduced. Required properties of a system are formally verified by deriving them from assumptions that themselves are properties of sub-components, which in their turn may be derived from assumptions on sub-sub-components, and so on. The method is based on properties that are formalized in terms of temporal semantics; both static and dynamic properties are covered. The compositional verification method imposes structure on the verification process. Because of the possibility of focusing at one level of abstraction (information and process hiding), compositional verification provides transparency and limits the complexity per level. Since verification proofs are structured in a compositional manner, they can be reused in the event of reuse of models or modification of an existing system. The method is illustrated for a generic model for diagnostic reasoning.     

Reducing the verification cost of evolving product families using static analysis techniques

Software product line engineering enables proactive reuse among a set of related products through explicit modeling of commonalities and differences among them. Software product lines are intended to be used in a long period of time. As a result, they evolve over time, due to the changes in the requirements. Having several individual products in a software family, verification of the entire family may take a considerable effort. In this paper we aim to decrease this cost by reducing the number of verified products using static analysis techniques. Furthermore, to reduce model checking costs after product line evolution, we restrict the number of products that should be re-verified by reusing the previous verification result. All proposed techniques are based on static analysis of the product family model with respect to the property and can be automated. To show the effectiveness of these techniques we apply them on a set of case studies and present the results.     

保护个人的利益——电子商务协议新属性的自动验证

电子商务的快速发展加强了电子商务协议的新类型的需求,尤其对各种复杂协议的需求,这使得协议本身安全性的证明变得更为困难。为了证明电子商务协议的可靠性,研究人员已设计了各种方法。为了更加清楚地描述需要证明的电子商务协议的安全目标,研究者们已经提出了几种标志性属性,其中之一是较著名的原子性犤8犦,但这并不能完全描述电子商务协议的全部安全性定义。在犤1犦里,研究员对一项有研究价值的新属性进行了研究,称为“保护个人的利益”,并且提出一个手工验证的模型。该模型虽然有效,但是实用性较差。文章提出了一个基于模型检验这种技术的自动验证方法。     

基于抽象和搜索空间划分的安全性判定方法

为满足访问控制策略安全性快速判定的要求,提出一种基于谓词抽象和验证空间划分的访问控制策略状态空间约减方法,将在访问控制策略原始状态机模型上的安全性分析工作转移到包含较少状态的抽象模型上,并进一步划分抽象模型的验证空间,以提高效率。理论分析和实验数据均表明,其安全性分析所需的时间和空间都得到有效约减。与传统方法相比,它具有速度更快、自动化程度更高等优点。