离散时段演算的符号模型验证

模型验证是对有限状态系统的一种形式化确认方法，近几年，模型验证方法已逐步扩展到实时系统应用中，为解决实时系统的模型验证问题，本文采用离散时段演算人实时系统规格说明的形式语言，用时间自动机作为实时系统的实现模型，对模型验证问题进行了细致的分析，并提出了一种具有实际应用价值的方法－商技术，该方法可以在避免当多个时间自动机并行组合时可能产生的状态空间组合爆炸问题，同时还可以简化整个模型验证问题。     

Stochastic automata network of modeling parallel systems

A methodology for modeling a system composed of parallel activities with synchronization points is proposed. Specifically, an approach based on a modular state-transition representation of a parallel system called the stochastic automata network (SAN) is developed. The state-space explosion is handled by a decomposition technique. The dynamic behavior of the algorithm is analyzed under Markovian assumptions. The transition matrix of the chain is automatically derived using tensor algebra operators, under a format which involves a very limited storage cost     

一类时间自动机的时间约束可满足性判定方法

时间自动机是一种有效描述实时系统行为的计算模型。借助时间自动机对实时系统进行分析、设计能够保证所开发的实时系统具有较高的可靠性。在此过程中对时间自动机的验证是非常关键的一步。验证的主要目的是为了保证时间自动机能够正确地描述实时系统。其中迁移的时间约束可满足性就是需要验证的性质之一。常用的方法是通过构造时间区域自动机来实现,但该方法所涉及的状态数目巨大。该文针对一类时间自动机的特点给出了基于时间关系矩阵来判定时间约束可满足性的方法,结果表明该方法能够有效地减少状态数。     

无人机飞控软件系统建模与测试用例生成研究

软件规模与复杂度的迅速增长已成为设计与检验现代高质量无人机飞行控制软件(FCS)系统的重要挑战。采用模型驱动工程(MDE)的框架,使用嵌入式实时系统建模语言(MARTE)建立起某型无人机飞控软件系统的模型,给出了基于时间自动机的系统动态行为的形式化模型实例;结合无人机FCS系统的应用背景,建立了基于时间自动机模型的测试用例生成方法,包括建立测试用例生成框架、测试用例生成规则以及用例生成策略等;对某型无人机飞控软件系统中的主控模块进行了建模与测试用例生成的实例分析研究。     

A practical data-flow verification scheme for business processes

Data in business processes becomes more and more important. Current standard languages for process modeling like BPMN 2.0 which include the data flow reflect this. Ensuring the correctness of the data flow in processes is challenging. Model checking, i.e., verifying properties of process models, is a well-known technique to this end. An important part of model checking is the construction of the state space of the model. However, state-space explosion typically is in the way of an effective verification. We study how to overcome this problem in our context by means of reduction. More specifically, we propose a reduction on the level of the process model. To our knowledge, this is new for the data-flow analysis of processes. The core of our approach are so-called regions of the process model that are relevant for the verification of properties describing the data flow. Non-relevant regions are candidates for reduction of the process model, yielding a smaller state space. Our evaluation shows that our approach works well on industrial process models.     

On-the-fly verification and optimization of DTA-properties for large Markov chains

We consider continuous-time Markov chains (CTMC) with very large or infinite state spaces which are, for instance, used to model biological processes or to evaluate the performance of computer and communication networks. We propose a numerical integration algorithm to approximate the probability that a process conforms to a specification that belongs to a subclass of deterministic timed automata (DTAs). We combat the state space explosion problem by using a dynamic state space that contains only the most relevant states. In this way we avoid an explicit construction of the state-transition graph of the composition of the DTA and the CTMC. We also show how to maximize the probability of acceptance of the DTA for parametric CTMCs and substantiate the usefulness of our approach with experimental results from biological case studies.     

Forward Analysis of Updatable Timed Automata

Timed automata are a widely studied model. Its decidability has been proved using the so-called region automaton construction. This construction provides a correct abstraction for the behaviours of timed automata, but it suffers from a state explosion and is thus not used in practice. Instead, algorithms based on the notion of zones are implemented using adapted data structures like DBMs. When we focus on forward analysis algorithms, the exact computation of all the successors of the initial configurations does not always terminate. Thus, some abstractions are often used to ensure termination, among which, a widening operator on zones.In this paper, we study in detail this widening operator and the corresponding forward analysis algorithm. This algorithm is most used and implemented in tools like KRONOS and UPPAAL. One of our main results is that it is hopeless to find a forward analysis algorithm for general timed automata, that uses such a widening operator, and which is correct. This goes really against what one could think. We then study in detail this algorithm in the more general framework of updatable timed automata, a model which has been introduced as a natural syntactic extension of classical timed automata. We describe subclasses of this model for which a correct widening operator can be found.     

A game-based abstraction-refinement framework for Markov decision processes

In the field of model checking, abstraction refinement has proved to be an extremely successful methodology for combating the state-space explosion problem. However, little practical progress has been made in the setting of probabilistic verification. In this paper we present a novel abstraction-refinement framework for Markov decision processes (MDPs), which are widely used for modelling and verifying systems that exhibit both probabilistic and nondeterministic behaviour. Our framework comprises an abstraction approach based on stochastic two-player games, two refinement methods and an efficient algorithm for an abstraction-refinement loop. The key idea behind the abstraction approach is to maintain a separation between nondeterminism present in the original MDP and nondeterminism introduced during the abstraction process, each type being represented by a different player in the game. Crucially, this allows lower and upper bounds to be computed for the values of reachability properties of the MDP. These give a quantitative measure of the quality of the abstraction and form the basis of the corresponding refinement methods. We describe a prototype implementation of our framework and present experimental results demonstrating automatic generation of compact, yet precise, abstractions for a large selection of real-world case studies.     

Compact Data Structures and State-Space Reduction for Model-Checking Real-Time Systems

During the past few years, a number of verification tools have been developed for real-time systems in the framework of timed automata. One of the major problems in applying these tools to industrial-sized systems is the huge memory-usage for the exploration of the state-space of a network (or product) of timed automata, as the model-checkers must keep information about not only the control structure of the automata but also the clock values specified by clock constraints. In this paper, we present a compact data structure for representing clock constraints. The data structure is based on an O(n ³) algorithm which, given a constraint system over real-valued variables consisting of bounds on differences, constructs an equivalent system with a minimal number of constraints. In addition, we have developed an on-the-fly reduction technique to minimize the space-usage. Based on static analysis of the control structure of a network of timed automata, we are able to compute a set of symbolic states that cover all the dynamic loops of the network in an on-the-fly searching algorithm, and thus ensure termination in reachability analysis. The two techniques and their combination have been implemented in the tool UPPAAL. Our experimental results demonstrate that the techniques result in truly significant space-reductions: for six examples from the literature, the space saving is between 75% and 94%, and in (nearly) all examples time-performance is improved. Noteworthy is also the observation that the two techniques are completely orthogonal.     

<Emphasis Type="Italic">SetExp</Emphasis>: a method of transformation of timed automata into finite state automata

Real-time discrete event systems are discrete event systems with timing constraints, and can be modeled by timed automata. The latter are convenient for modeling real-time discrete event systems. However, due to their infinite state space, timed automata are not suitable for studying real-time discrete event systems. On the other hand, finite state automata, as the name suggests, are convenient for modeling and studying non-real time discrete event systems. To take into account the advantages of finite state automata, an approach for studying real-time discrete event systems is to transform, by abstraction, the timed automata modeling them into finite state automata which describe the same behaviors. Then, studies are performed on the finite state automata model by adapting methods designed for non real-time discrete event systems. In this paper, we present a method for transforming timed automata into special finite state automata called Set-Exp automata. The method, called SetExp, models the passing of time as real events in two types: Set events which correspond to resets with programming of clocks, and Exp events which correspond to the expiration of clocks. These events allow to express the timing constraints as events order constraints. SetExp limits the state space explosion problem in comparison to other transformation methods of timed automata, notably when the magnitude of the constants used to express the timing constraints are high. Moreover, SetExp is suitable, for example, in supervisory control and conformance testing of real-time discrete event systems.     

一种基于时间自动机的域构造方法

模型检验是一种重要的形式化自动验证技术,通过状态空间搜索来保证软硬件设计的正确性。由于TCTL不是针对时间自动机,而是针对有限状态变迁系统的,从而无法使用TCTL直接对时间自动机进行模型检验。给出了一种从时间自动机到有限状态变迁系统的方法,并在不改变时间自动机的语义上,使时间自动机等价后的域状态数尽可能少,在一定程度上有效地解决了状态空间爆炸问题。     

模型检测新技术研究

1 引言软件是否可信赖已成为一个国家的经济、国防等系统能否正常运转的关键因素之一,尤其在一些诸如核反应堆控制、航空航天以及铁路调度等安全悠关(safety-critical)领域更是如此。这类系统要求绝对安全可靠,不容半点疏漏,否则将导致灾难性后果。如1996年6月4日,欧洲航天局阿丽亚娜(Ariane)501火箭因为其控制软件的规范和设计错误而导致发射37秒后爆炸。类似的报道屡见不鲜,如何确保这些系统的可靠性成为计算机科学与控制论领域共同关注的一个焦点问题。     

Template languages for fault monitoring of timed discrete eventprocesses

This paper introduces a new framework for modeling discrete event processes. This framework, called condition templates, allows the modeling of processes in which both single-instance and multiple-instance behaviors are exhibited concurrently. A single-instance behavior corresponds to a trace from a single finite-state process, and a multiple-instance behavior corresponds to the timed interleavings of an unspecified number of identical processes operating at the same time. The template framework allows the modeling of correct operation for systems consisting of concurrent mixtures of both single and multiple-instance behaviors. This representation can then be used in online fault monitoring for confirming the correct operation of a system. We compare the class of timed languages representable by template models with classes of timed languages from timed automata models. It is shown that templates are able to model timed languages corresponding to single and multiple-instance behaviors and combinations thereof. Templates can thus represent languages that could not be represented or monitored using timed automata alone     

Model-checking timed automata with deadlines with Uppaal

Timed automata with deadlines (TAD) are a form of timed automata that admit a more natural representation of urgent actions, with the additional advantage of avoiding the most common form of timelocks. We offer a compositional translation of a practically useful subset of TAD to timed safety automata (the well-known variant of timed automata where time progress conditions are expressed by invariants). More precisely, we translate networks of TAD to the modeling language of Uppaal, a state-of-the-art verification tool for timed automata. We also describe an implementation of this translation, which allows Uppaal to aid the design and analysis of TAD models.     

The SH-Verification Tool — Abstraction-Based Verification of Co-operating Systems

The sh-verification tool comprises computing abstractions of finite-state behaviour representations as well as automata and temporal logic based verification approaches. To be suitable for the verification of so called co-operating systems, a modified type of satisfaction relation (approximate satisfaction) is considered. Regarding abstraction, alphabetic language homomorphisms are used to compute abstract behaviours. To avoid loss of important information when moving to the abstract level, abstracting homomorphisms have to satisfy a certain property called simplicity on the concrete (i.e. not abstracted) behaviour. The well known state space explosion problem is tackled by a compositional method combined with a partial order method. Received March 1997 / Accepted in revised form July 1998     

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

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

Axiomatising timed automata

Timed automata has been developed as a basic semantic model for real time systems. Its algorithmic aspects for automated analysis have been well studied. But so far there is still no satisfactory algebraic theory to allow the derivation of semantical equivalence of automata by purely syntactical manipulation. The aim of this paper is to provide such a theory. We present an inference system of timed bisimulation equivalence for timed automata based on a CCS-style regular language for describing timed automata. It consists of the standard monoid laws for bisimulation and a set of inference rules. The judgments of the proof system are conditional equations of the form where is a clock constraint and t,u are terms denoting timed automata. The inference system is shown to be sound and complete for timed bisimulation. The proof of the completeness result relies on the notion of symbolic timed bisimulation, adapted from the work on value–passing processes. Received: 10 May 2001 / 22 October 2001     

Bounded Model Checking for Timed Automata

Given a timed automaton M, a linear temporal logic formula φ, and a bound k, bounded model checking for timed automata determines if there is a falsifying path of length k to the hypothesis that M satisfies the specification φ. This problem can be reduced to the satisfiability problem for Boolean constraint formulas over linear arithmetic constraints. We show that bounded model checking for timed automata is complete, and we give lower and upper bounds for the length k of counterexamples. Moreover, we define bounded model checking for networks of timed automata in a compositional way.     

Equivalence of dynamical systems by bisimulation

A general notion of bisimulation is defined for linear input-state-output systems, using analogies with the theory of concurrent processes. A characterization of bisimulation and an algorithm for computing the maximal bisimulation relation is derived using geometric control theory. Bisimulation is shown to be a notion which unifies the concepts of state-space equivalence and state-space reduction, and which allows to study equivalence of systems with nonminimal state-space dimension. The notion of bisimulation is especially powerful for "nondeterministic" dynamical systems, and leads in this case to a notion of equivalence which is finer than equality of external behavior. For abstractions of systems it is shown how the results specialize to previously obtained results by other authors. Extensions of the main results to the nonlinear case are provided.     

构件式实时系统建模与验证研究

在复杂的实时系统开发中使用构件式设计方法已成为目前软件开发领域中的研究热点,如何有效地验证实时软件的设计是否满足给定的时间需求并降低验证过程的复杂度,是实时计算领域中的主要挑战之一.文中对构件接口模型进行时间扩展,提出了时间接口模型,并将其用于构件接口交互行为的形式化建模.在接口自动机理论的的基础上进一步提出了时间接口自动机模型用于描述时间接口交互下构件的行为及组合方法,通过消除错误状态产生组合模型来约减构件时间接口自动机模型的积,并在约减的模型上进行性质检验,降低了分析复杂度,有效地应对状态空间爆炸问题.为了说明论文建议的方法,详细讨论了一个简单的、贯穿整篇论文的示例系统.