Safety verification and reachability analysis for hybrid systems

Safety verification and reachability analysis for hybrid systems is a very active research domain. Many approaches that seem quite different, have been proposed to solve this complex problem. This paper presents an overview of various approaches for autonomous, continuous-time hybrid systems and presents them with respect to basic problems related to verification.     

Computation of maximal reachability submodules

A new and conceptually simple procedure is derived for the computation of the maximal reachability submodule of a given submodule of the state space of a linear discrete-time system over a Noethenian ring R. The procedure is effective if R is effective and if kernels and intersections can be computed. The procedure is compared with a rather different procedure by Assan e.a. published recently.     

Reverse reachability analysis: A new technique for deadlock detection on communicating finite state machines

The communicating finite state machines can exchange messages over bounded FIFO channels. In this paper, a new technique, called reverse reachability analysis, is proposed to detect deadlocks on the communication between the communicating finite state machines. The technique is based on finding reverse reachable paths starting from possible deadlock states. If a reverse reachable path can reach the initial global state, then deadlock occurs. Otherwise the communication is deadlock-free. The effectiveness of the technique has been verified by some real protocols such as a specification of X.25 call establishment/clear protocol and Bartlet's alternating bit protocol.     

An approach to cyclic protocol validation

In this paper, the notion of fair reachability is generalized to cyclic protocols with more than two processes, where all the processes in a protocol are connected via a unidirectional ring and each process might contain internal transitions and can be non-deterministic. We identify ‘indefiniteness’ as a new type of logical error due to reachable internal transition cycles. By properly incorporating internal transitions into the formulation, we show that, with a few modifications, all the previous results established for cyclic protocols without non-deterministic and internal transitions still hold in the augmented model. Furthermore, by combining fair progress and maximal progress during state exploration, we prove that the following three problems are all decidable for Q, the class of cyclic protocols with finite fair reachable state spaces: (1) global state reachability; (2) abstract state reachability; and (3) execution cycle reachability. In the course of the investigation, we also show that detection of k-indefiniteness and k-livelock are decidable for Q.     

Exponential space complexity for OBDD-based reachability analysis

Ordered binary decision diagrams (OBDDs) are one of the most common dynamic data structures for Boolean functions. Nevertheless, many basic graph problems are known to be PSPACE-hard if their input graphs are represented by OBDDs. Computing the set of nodes that are reachable from some source s∈V in a digraph G=(V,E) is an important problem in computer-aided design, hardware verification, and model checking. Until now only exponential lower bounds on the space complexity of a restricted class of OBDD-based algorithms for the reachability problem have been known. Here, the result is extended by presenting an exponential lower bound for the general reachability problem. As a by-product a general exponential lower bound is obtained for the computation of OBDDs representing all connected node pairs in a graph, the transitive closure.     

Implementation and analysis of real-time communication protocol compositions

A flexible way of building modular communication stacks relies on the use of protocol composition. This paper describes a protocol composition framework that simplifies the task of deriving the worst-case response time of a protocol composition from the protocol implementation. In order to derive the worst-case response time of a protocol composition, one needs to capture its event-graph: the event-graph consists of the set of all events processed by each component and the relation between those events. The framework, called RT-Appia, takes a pragmatic approach: instead of requiring the use of domain specific code analysis tools, or dedicated compilers, it simply requires protocol programmers to make explicit which events are processed and produced by each layer, and how these events are related. An interesting aspect of the approach is that the same data structures that are used to simplify the task of computing the worst-case response time of the protocol composition are also used to optimize the performance and to debug the resulting implementation.

State space analysis of Petri nets with relation-algebraic methods

A large variety of systems can be modelled by Petri nets. Their formal semantics are based on linear algebra which in particular allows the calculation of a Petri net’s state space. Since state space explosion is still a serious problem, efficiently calculating, representing, and analysing the state space is mandatory. We propose a formal semantics of Petri nets based on executable relation-algebraic specifications. Thereupon, we suggest how to calculate the markings reachable from a given one simultaneously. We provide an efficient representation of reachability graphs and show in a correct-by-construction approach how to efficiently analyse their properties. Therewith we cover two aspects: modelling and model checking systems by means of one and the same logic-based approach. On a practical side, we explore the power and limits of relation-algebraic concepts for concurrent system analysis.     

Ellipsoidal techniques for reachability analysis: internal approximation

For the reach tube of a linear time-varying system with ellipsoidal bounds on the control variable consider the following approximation problem. Find a tight ellipsoid-valued tube inside the reach tube that touches it along any prespecified smooth curve on the boundary. We construct this ellipsoidal tube, and show that if the given curve is itself a system trajectory, the tube can be calculated recursively, with minimum computational burden.     

Verification of the Capability Exchange Signalling protocol

The Capability Exchange Signalling (CES) protocol is one of the sub-protocols of recommendation H.245, “Control protocol for multimedia communication” issued by the International Telecommunication Union. In this paper, we model the CES protocol with Coloured Petri Nets and verify it using state space and language analyses. The results reveal that the CES protocol could fail when the sequence numbers used by the protocol wrap. To solve this problem, we propose a set of changes to the CES protocol. State space and language analyses are then applied to the revised protocol. Verification results suggest that the revised protocol satisfies the desired properties with the errors discovered being eliminated.     

A work-efficient distributed algorithm for reachability analysis

This work presents a novel distributed symbolic algorithm for reachability analysis that can effectively exploit, as needed, a large number of machines working in parallel. The novelty of the algorithm is in its dynamic allocation and reallocation of processes to tasks and in its mechanism for recovery from local state explosion. As a result, the algorithm is work-efficient: it utilizes only those resources that are actually needed. In addition, its high adaptability makes it suitable for exploiting the resources of very large and heterogeneous distributed, nondedicated environments. Thus, it suitable for verifying very large systems. We implemented our algorithm in a tool called Division. Our experimental results show that the algorithm is indeed work-efficient. Although the goal of this research is to check larger models, the results also indicate that the algorithm can obtain high speedups, because communication overhead is very small.     

Feedback-reversibility and reachability of linear impulsive systems

For a linear impulsive system, the set of states that are reachable from the origin when the initial time, impulse times, and final time are fixed is contained in an invariant subspace determined by the system data. It is known that reversibility of the system is sufficient to yield, for a specified initial time, the existence of some impulse time set and final time for which the reachable set equals the invariant subspace. In this paper, we relax the reversibility requirement and present a condition that is necessary as well as sufficient under which this property holds. This new condition involves the property of achieving reversibility via feedback and admits an explicit geometric characterization. Moreover, this feedback-reversibility property only needs to hold for the subsystem defined as the full system restricted to the invariant subspace. We further show that feedback-reversibility of the restricted system ensures that the reachable set equals the invariant subspace for almost any impulse time set and final time for which the number of impulse times contained in the underlying time interval exceeds a lower bound.     

一种基于ECB模式的NSL协议改进方案

安全协议形式化方法大都在一个很高的抽象层次建立协议模型。但是协议的许多安全问题是在很低的抽象层次产生。本文分析了ECB工作模式下的NSL协议的安全问题,并通过破坏同态性的方法给出一种改进方案。通过扩展规则的BAN逻辑对NSL协议建模和分析,验证结果表明协议中存在着安全漏洞,新的改进方案可以避免这种攻击。     

时间自动机可达性分析中的状态空间约减技术综述

时间自动机是检验实时系统建模的有效工具,其可达性分析可以检验系统是否可能达到某些特定的状态,其算法通常采用对符号状态的枚举来遍历其状态空间。因为引入了时钟变量,时间自动机的可达性分析算法会产生大量的中间状态,需要巨大的存储空间,往往超出了计算机能力的极限,导致分析和检验不能完成。这就是所谓的“状态空间爆炸”。研究人员设计了很多种优化技术来约减可迭性分析所需的存储空间,以解决或者缓解这个问题。本文首先介绍了时间自动机及其可达性分析的基本概念,然后分类讨论了现有的空间约减优化技术并对此做出总结,最后提出了一些未来的研究方向。     

形状分析符号执行引擎中的状态合并

符号执行技术以其良好的精确度控制和代码覆盖率被广泛应用于静态程序分析和高覆盖率测试用例自动生成。 符号执行 在分析程序时,以模拟真实的程序执行过程的方式分析程序的数据流和控制流信息,并检查程序可能出现的所有状态,得到程序的分析结果。高精确度和高覆盖率要求对程序状态描述具体而完备,这会导致符号执行过程中常见的状态爆炸问题。首先提出在不同的执行路径上对具体内存状态进行合并的算法,然后对内存模型进行适度的抽象,扩大状态合并算法的适用范围,最后讨论状态合并所带来的实际效果,并提出了状态合并的优化解决方案。所提出的算法在符号执行引擎ShapeChecker上实现,并取得了良好的实验结果。     

SHAPA: an interactive software environment for protocol analysis

This paper briefly reviews work on verbal report and describes SHAPA, an interactive program for performing both verbal and non-verbal protocol analysis. To a certain extent, SHAPA is to protocol data what a spreadsheet program is to numerical data or what a word processor is to text it is intelligent about the sorts of things a researcher might want to do with verbal or non-verbal protocols, while being blind to particular domains, contexts, or theories. It has been developed with the idea of affording the researcher the closest possible degree of engagement with protocol data. The researcher can configure SHAPA to encode protocols using a wide variety of theoretical frameworks or vocabularies. SHAPA allows protocol analysis to be performed at any level of analysis, and it supplies many tools for data aggregation, manipulation and analysis. Some of these tools have been imported from a tradition of work on non-verbal protocol analysis that has developed very strong analytical tools. The output generated by SHAPA can be used alone or in combination with other performance variables to get a rich picture of the influences on sequences of verbal or non-verbal behaviour.     

Uncovering ISO ROSE protocol errors using Estelle

One of the main objectives of ISO in developing FDTs is that protocol specified in them can be verified. However, standardized FDTs have been designed largely for specification purpose; success of using them for protocol verification has been rarely reported. We have developed a technique of translating Estelle specifications into Numerical Petri nets, which can then be verified by a proven automated verification tool, PROTEAN. The merits of our approach are that specifications are fully based on standard Estelle, and dynamic behaviours of an Estelle specification can be handled. In this paper, we present a success story of using Estelle and the techniques we have developed to uncover ISO ROSE protocol errors. We find that Estelle is an FDT capable of analysing and verifying real protocols and it is therefore important to the development of ISO protocol standards.     

Decision-diagram-based techniques for bounded reachability checking of asynchronous systems

Bounded reachability analysis and bounded model checking are widely believed to perform poorly when using decision diagrams instead of SAT procedures. Recent research suggests this to be untrue with regards to synchronous systems and, in particular, digital circuits. This article shows that the belief is also a myth for asynchronous systems, such as models specified by Petri nets. We propose several Bounded Saturation approaches to compute bounded state spaces using decision diagrams. These approaches are based on the established Saturation algorithm, which benefits from a non-standard search strategy that is very different from breadth-first search, but employ different flavors of decision diagrams: multi-valued decision diagrams, edge-valued decision diagrams, and algebraic decision diagrams. We apply our approaches to studying deadlock as a safety property. Our extensive benchmarking shows that our algorithms often, but not always, compare favorably against two SAT-based approaches that are advocated in the literature. Research supported by the NSF under grants CNS-0501747 and CNS-0501748 and by the EPSRC under grant GR/S86211/01. An extended abstract of this article appeared in the proceedings of the 13th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS~4424, pp.~648–663, 2007, Springer.     

An improved protocol validation technique for a class of communication models

The topology of a communication network is often represented by a directed labeled graph in which there exists one and only one elementary path from one node to any other node, where nodes and arcs in the graph represent the processes in the communication network and the links between the processes, respectively. In this paper, we propose an algorithm for the validation of the protocols, represented by N (N ⩾ 2) communicating finite state machines, in the restricted class of the communication networks with such topology. The algorithm can detect deadlocks and unspecified receptions, and saves time and/or storage in comparison with the conventional perturbation technique.