实时系统的模型检验中针对共享变量的优化技术

实时系统可以使用由多个并发的时间自动机组成的时间自动机网络来建模。网络中的时间自动机通过共享变量和/或信道交互。带有不同共享变量取值的自动机网络的状态是截然不同的。因此,共享变量也是引起状态空间爆炸问题的原因之一。本文提出了在不同共享变量取值之间的兼容性关系的概念。使用这种兼容性关系,时间自动机网络的可达性分析算法就可以减少需要遍历的状态的个数。本文给出了检测符号化状态中共享变量的取值所能兼容的其它取值的算法以及进一步进行这种兼容性关系检测的增强算法。最后还给出了使用了这两种算法进行优化之后的可迭性分析算法。实验结果显示经优化的可达性分析算法的空间效率得到了显著的提高。     

Introductory Paper

In today’s competitive market designing of digital systems (hardware as well as software) faces tremendous challenges. In fact, notwithstanding an ever decreasing project budget, time to market and product lifetime, designers are faced with an ever increasing system complexity and customer expected quality. The above situation calls for better and better formal verification techniques at all steps of the design flow. This special issue is devoted to publishing revised versions of contributions first presented at the 12th Advanced Research Working Conference on Correct Hardware Design and Verification Methods (CHARME) held 21–24 October 2003 in L’Aquila, Italy. Authors of well regarded papers from CHARME’03 were invited to submit to this special issue. All papers included here have been suitably extended and have undergone an independent round of reviewing.     

一种基于模型检测的二进制程序脆弱性分析框架

针对二进制程序脆弱性分析的实际需求,提出了一种基于模型检测的二进制程序脆弱性分析框架。首先定义了二进制程序的抽象模型,描述了基于有限状态自动机的软件脆弱性形式化表示和基于事件系统的软件安全属性表示方法。在此基础上,提出了基于模型检测的脆弱性分析过程和算法。根据该分析框架,设计并实现了二进制程序脆弱性分析工具原型。通过脆弱性分析实验,详细说明了该框架的工作原理,验证了该分析方法的有效性。     

State-rich model checking

In this paper we survey the area of formal verification techniques, with emphasis on model checking due to its wide acceptance by both academia and industry. The major approaches and their characteristics are presented, together with the main problems faced while trying to apply them. With the increased complexity of systems, as well as interest in software correctness, the demand for more powerful automatic techniques is pushing the theories and tools towards integration. We discuss the state of the art in combining formal methods tools, mainly model checking with theorem proving and abstract interpretation. In particular, we present our own recent contribution on an approach to integrate model checking and theorem proving to handle state-rich systems specified using a combination of Z and CSP.     

SOCKET通信程序模型抽取及可靠性验证

形式化方法是验证并发系统可靠性和安全性的重要手段。对高级语言开发的并发系统自动抽取的模型进行形式化验证是模型检测技术领域中的一个研究热点。鉴于socket函数调用顺序不正确产生的运行时潜在问题(内存泄漏、死锁、边界数据丢失等),针对顺序结构的socket程序,通过描述Promcla消息数据结构和通道,构建socket函数的Promcla模型,定义socket函数到Promcla映射规则,提出socket函数调用序列抽取算法及目标Promcla模型生成算法,用线性时态逻辑(LTI.)刻画socket函数调用顺序应满足的性质,开发基于SPIN的socket通信程序分析系统。实验结果表明,该系统能有效检测socket通信程序的运行时潜在问题。     

模型检测技术和密码协议分析

1 引言密码协议是建立在密码体制基础上的一种交互通信的协议,它运行在计算机通信网或分布式系统中,借助于密码算法来达到密钥分配、身份认证等目的。目前密码协议已广泛应用于计算机通信网与分布式系统中,但密码协议安全性的论证仍是一个悬而未决的问题。九十年代以来,密码协议的形式化分析成为国际上的研究热点。这种方法的出发点是希望将密码协议形式化,而后借助于人工推导,甚至计算机的辅助分析,     

SET协议形式化分析与模型检测

随着移动网络技术的快速发展,电子商务的大量普及,电子商务不在单单只是局限于有线网络,商家们开始将商机延续到移动网络。移动网络用户群体中手机移动上网用户占绝大部分,在这样的商机驱动下,移动电子商务得到快速发展。移动电子商务中最为核心的技术是移动电子支付协议SET,它直接决定了移动电子商务的安全性、高效性。本文就在这样的背景下采用AVISPA工具研究SET协议,通过形式化分析与模型检测,发现了SET协议的支付密钥的不安全性,并给出了攻击路径。     

Using SPIN to Analyse the Tree Identification Phase of the IEEE 1394 High-Performance Serial Bus (FireWire) Protocol

We describe how the tree identification phase of the IEEE 1394 high-performance serial bus (FireWire) protocol is modelled in Promela and verified using SPIN. The verification of arbitrary system configurations is discussed. Received July 2001/Accepted in revised form November 2002 Correspondence and offprint requests to: Alice Miller, Department of Computing Science, University of Glasgow, 17 Lilybank Gardens, Glasgow G12 8QQ, UK. Email: alice@dcs.gla.ac.uk     

Specifying and analyzing early requirements in Tropos

We present a framework that supports the formal verification of early requirements specifications. The framework is based on Formal Tropos, a specification language that adopts primitive concepts for modeling early requirements (such as actor, goal, and strategic dependency), along with a rich temporal specification language. We show how existing formal analysis techniques, and in particular model checking, can be adapted for the automatic verification of Formal Tropos specifications. These techniques have been implemented in a tool, called the T-Tool, that maps Formal Tropos specifications into a language that can be handled by the NuSMV model checker. Finally, we evaluate our methodology on a course-exam management case study. Our experiments show that formal analysis reveals gaps and inconsistencies in early requirements specifications that are by no means trivial to discover without the help of formal analysis tools.

基于动态内存和状态管理的模型检测新方法

模型检测是并发系统验证的主要形式化方法之一,但其存在因状态空间爆炸而导致内存不够的问题,这也是大规模并发系统验证的瓶颈.很多研究人员尽管做了很多相关研究,但仍然没有很好地解决这个问题.在研究动态内存和状态管理的基础上,提出了一种新的模型检测方法,避免了因为内存不足而无法模型检测的问题.     

Coverage metrics for formal verification

In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proven to be correct, there is still a question of how complete the specification is and whether it really covers all the behaviors of the system. The challenge of making the verification process as exhaustive as possible is even more crucial in simulation-based verification, where the infeasible task of checking all input sequences is replaced by checking a test suite consisting of a finite subset of them. It is very important to measure the exhaustiveness of the test suite, and indeed there has been extensive research in the simulation-based verification community on coverage metrics, which provide such a measure. It turns out that no single measure can be absolute, leading to the development of numerous coverage metrics whose usage is determined by industrial verification methodologies. On the other hand, prior research of coverage in formal verification has focused solely on state-based coverage. In this paper we adapt the work done on coverage in simulation-based verification to the formal-verification setting in order to obtain new coverage metrics. Thus, for each of the metrics used in simulation-based verification, we present a corresponding metric that is suitable for the setting of formal verification and describe an algorithmic way to check it.     

Automated formal verification of visual modeling languages by model checking

Graph transformation has recently become more and more popular as a general, rule-based visual specification paradigm to formally capture (a) requirements or behavior of user models (on the model-level), and (b) the operational semantics of modeling languages (on the meta-level) as demonstrated by benchmark applications around the Unified Modeling Language (UML). The current paper focuses on the model checking-based automated formal verification of graph transformation systems used either on the model-level or meta-level. We present a general translation that inputs (i) a metamodel of an arbitrary visual modeling language, (ii) a set of graph transformation rules that defines a formal operational semantics for the language, and (iii) an arbitrary well-formed model instance of the language and generates a transitions system (TS) that serve as the underlying mathematical specification formalism of various model checker tools. The main theoretical benefit of our approach is an optimization technique that projects only the dynamic parts of the graph transformation system into the target transition system, which results in a drastical reduction in the state space. The main practical benefit is the use of existing back-end model checker tools, which directly provides formal verification facilities (without additional efforts required to implement an analysis tool) for many practical applications captured in a very high-level visual notation. The practical feasibility of the approach is demonstrated by modeling and analyzing the well-known verification benchmark of dining philosophers both on the model and meta-level.     

Coverage metrics for temporal logic model checking*

In formal verification, we verify that a system is correct with respect to a specification. Even when the system is proved to be correct, there is still a question of how complete the specification is, and whether it really covers all the behaviors of the system. In this paper we study coverage metrics for model checking. Coverage metrics are based on modifications we apply to the system in order to check which parts of it were actually relevant for the verification process to succeed. We introduce two principles that we believe should be part of any coverage metric for model checking: a distinction between state-based and logic-based coverage, and a distinction between the system and its environment. We suggest several coverage metrics that apply these principles, and we describe two algorithms for finding the non-covered parts of the system under these definitions. The first algorithm is a symbolic implementation of a naive algorithm that model checks many variants of the original system. The second algorithm improves the naive algorithm by exploiting overlaps in the variants. We also suggest a few helpful outputs to the user, once the non-covered parts are found.

Mu-calculus path checking

We investigate the path model checking problem for the μ-calculus. Surprisingly, restricting to deterministic structures does not allow for more efficient model checking algorithm, as we prove that it can encode any instance of the standard model checking problem for the μ-calculus.     

模型检测中状态爆炸问题研究综述

模型检测已成为保证软件系统正确性和可靠性的重要手段,但随着软件功能日益强大,其规模和复杂度也越来越大,在模型检测过程中容易产生状态爆炸问题。如何解决模型检测中的状态爆炸,已成为工业界和理论界无法回避的重要课题。系统地综述模型检测领域解决状态爆炸问题的关键技术和主要方法,并提出该领域的最新研究进展与方向。     

Using probabilistic model checking for dynamic power management

Dynamic power management (DPM) refers to the use of runtime strategies in order to achieve a tradeoff between the performance and power consumption of a system and its components. We present an approach to analysing stochastic DPM strategies using probabilistic model checking as the formal framework. This is a novel application of probabilistic model checking to the area of system design. This approach allows us to obtain performance measures of strategies by automated analytical means without expensive simulations. Moreover, one can formally establish various probabilistically quantified properties pertaining to buffer sizes, delays, energy usage etc., for each derived strategy.Received November 2003Revised September 2004Accepted December 2004 by M. Leuschel and D. J. Cooke     

模型检验软件体系结构研究与进展

软件体系结构经过10多年的发展,在体系结构的基础理论、体系结构风格、体系结构描述语言和体系结构建模等方面的研究取得了一系列可喜的成就。目前,就软件体系结构的分析、评价、测试和验证的研究也在如火如荼地进行中。模型检验是一种基于自动机理论的形式验证方法,采用穷举状态空间的方式来证明系统的模型是否满足要验证的属性。同传统的测试和验证的手段相比,模型检验有其自身的优势。为此,越来越多的研究人员正在将模型检验技术应用到软件体系结构的分析和验证中。本文调查了模型检验技术在软件体系结构中的应用现状,剖析了影响软件体系结构模型检验的因素,给出了软件体系结构模型检验的未来主题。     

基于CDFG和OVL的系统验证性质分类

在数据控制流图（CDFG）结构的基础上,结合模拟验证和模型检测的优点,对需要验证的系统性质进行分类,采用不同的验证方法,提高验证的能力,通过对OVL语言和CTL描述进行改进,针对模拟验证,CDFG图匹配,模型检测3种方法设计相应的性质,实验结果表明这种分治验证策略有助于提高系统验证的效率和规模。