On the computational complexity of bisimulation, redux

Paris Kanellakis and the second author (Smolka) were among the first to investigate the computational complexity of bisimulation, and the first and third authors (Moller and Srba) have long-established track records in the field. Smolka and Moller have also written a brief survey about the computational complexity of bisimulation [ACM Comput. Surv. 27(2) (1995) 287]. The authors believe that the special issue of Information and Computation devoted to PCK50: Principles of Computing and Knowledge: Paris C. Kanellakis Memorial Workshop represents an ideal opportunity for an up-to-date look at the subject.     

一类并发实时系统的自动验证

一个被广泛用于验证实时系统的方法是根据被验证的实时性质,使用适当的双向模拟等价关系使无限的状态空间转化为有限的状态等价类空间.算法只需要在这个有限的等价类空间里搜索就可以得到正确答案.但是,这个等价类空间的规模一般随着系统规模的增大而产生爆炸性的增长,以至于在很多情况下,穷尽搜索这个空间是不现实的.该文引入了一个等价关系来验证一个由多个实时自动机通过共享变量组成的并发系统是否满足一个线性时段特性.同时,还引入了格局之间的兼容关系来避免对状态等价类空间的穷尽搜索.基于这两个关系,文章提出了一个算法来验证是否一个实时自动机网满足一个线性时段特性.实例研究显示,此算法在某些情况下比其他一些工具有更好的时间和空间效率.     

Before and after CASE adoption

Various authors and companies claim that the CASE technology increases both the quality and productivity of systems development. However, although the literature is replete with reports of successful adoption, many companies have not adopted it. This paper addresses the major reasons for companies' adoption of CASE and the major obstacles preventing the adoption. Furthermore, the authors investigated the changes in systems development practices in the light of the CASE technology. Finally, we determined the extent to which companies use and appreciate CASE. The authors analyzed 253 returned surveys to shed light on the questions: How do CASE users differ from non-users, and what are the differences between systems development practices before and after CASE adoption? They found that the CASE users spend more time during the front-end SDLC phases, use standard systems development techniques more often, and experience less difficulty during systems development.     

Responsiveness and stable revivals

Individual components in an inter-operating system require assurance from other components both of appropriate functionality and of suitable responsiveness. We have developed properties which capture the notion of non-blocking responsive behaviour, together with machine-based checks implemented in the CSP model-checker, FDR. In this paper we illustrate the use of our responsiveness properties with a small example, and provide a detailed comparison to related work in CCS. This work has led to the discovery of a new semantic model for CSP with respect to which such properties are fully abstract. We present the new stable revivals model and discuss implications for responsiveness checking. R. Lazic, R. Nagarajan and J. C. P. Woodcock     

Model-checking dense-time Duration Calculus

Since the seminal work of Zhou Chaochen, M. R. Hansen, and P. Sestoft on decidability of dense-time Duration Calculus [ZHS93] it is well known that decidable fragments of Duration Calculus can only be obtained through withdrawal of much of the interesting vocabulary of this logic. While this was formerly taken as an indication that key-press verification of implementations with respect to elaborate Duration Calculus specifications were also impossible, we show that the model property is well decidable for realistic designs which feature natural constraints on their switching dynamics.The key issue is that the classical undecidability results rely on a notion of validity of a formula that refers to a class of models which is considerably richer than the possible behaviours of actual embedded real-time systems: that of finitely variable trajectories. By analysing two suitably sparser model classes we obtain model-checking procedures for rich subsets of Duration Calculus. Together with undecidability results also obtained, this sheds light upon the exact borderline between decidability and undecidability of Duration Calculi and related logics.Received June 1999Accepted in revised form September 2003 by M. R. Hansen and C. B. Jones     

真空变化对火电机组协调控制策略修正方法的研究及实现

真空是机组运行监视的主要参数之一,它关系到机组的安垒运行,决定了机组的理想焓降、发电效率和出力能力.在以往的机组控制中,仅把真空作为机组的保护参数,而没有将真空变化对控制参数的影响考虑在内,使得机组在真空不同时控制调节品质相差较多.本文介绍了通过试验方法获取真空改变对机组运行状态的影响数据,增加协调控制中对真空的修正部分达到控制优化目的试验过程.     

Modular strategies for recursive game graphs

Many problems in formal verification and program analysis can be formalized as computing winning strategies for two-player games on graphs. In this paper, we focus on solving games in recursive game graphs which can model the control flow in sequential programs with recursive procedure calls. While such games can be viewed as the pushdown games studied in the literature, the natural notion of winning in our framework requires the strategies to be modular with only local memory; that is, resolution of choices within a module does not depend on the context in which the module is invoked, but only on the history within the current invocation of the module. While reachability in (global) pushdown games is known to be EXPTIME-complete, we show reachability in modular games to be NP-complete. We present a fixed-point computation algorithm for solving modular games such that in the worst case the number of iterations is exponential in the total number of returned values from the modules. If the strategy within a module does not depend on the global history, but can remember the history of the past invocations of this module, that is, if memory is local but persistent, we show that reachability becomes undecidable.     

Design and verification of a coordination protocol for cooperating systems

 This paper proposes an approach to producing a verified design of a complex intelligent system. The system is modeled using a hierarchical structure based on a coordination protocol. The coordination protocol and the system architecture are described using a state machine representation. The Clarke-McMillan Symbolic Model Checker based on branching time temporal logic is used to verify some of the desired formal properties of the protocol such as completeness, boundedness and termination. This work shows that the model checker helps to bring the automatic verification of complex intelligent systems closer to a practical proposition.     

Model-checking games for fixpoint logics with partial order models

In this paper, we introduce model-checking games that allow local second-order power on sets of independent transitions in the underlying partial order models where the games are played. Since the interleaving semantics of such models is not considered, some problems that may arise when using interleaving representations are avoided and new decidability results for partial order models of concurrency are achieved. The games are shown to be sound and complete, and therefore determined. While in the interleaving case they coincide with the local model-checking games for the μ-calculus, in a partial order setting they verify properties of a number of fixpoint modal logics that can specify, in concurrent systems with partial order semantics, several properties not expressible with the μ-calculus. The games underpin a novel decision procedure for model-checking all temporal properties of a class of infinite and regular event structures, thus improving, in terms of temporal expressive power, previous results in the literature.     

Model-checking discrete duration calculus

Duration Calculus was introduced in [ZHR91] as a logic to specify and reason about requirements for real-time systems. It is an extension of Interval Temporal Logic [Mos85] where one can reason about integrated constraints over time-dependent and Boolean valued states without explicit mention of absolute time. Several major case studies, e.g. the gas burner system in [RRH93], have shown that Duration Calculus provides a high level of abstraction for both expressing and reasoning about specifications. Using Timed Automata [A1D92] one can express how real-time systems can be constructed at a level of detail which is close to an actual implementation. We consider in the paper the correctness of Timed Automata with respect to Duration Calculus formulae. For a subset of Duration Calculus, we show that one can automatically verify whether a Timed Automaton is correct with respect to a formulaD, abbreviated D, i.e. one can domodel-checking. The subset we consider is expressive enough to formalize the requirements to the gas burner system given in [RRH93]; but only for a discrete time domain. Model-checking is done by reducing the correctness problem D to the inclusion problem of regular languages.     

Compiling and verifying SC-SystemJ programs for safety-critical reactive systems

Most of today's embedded systems are very complex. These systems, controlled by computer programs, continuously interact with their physical environments through network of sensory input and output devices. Consequently, the operations of such embedded systems are highly reactive and concurrent. Since embedded systems are deployed in many safety-critical applications, where failures can lead to catastrophic events, an approach that combines mathematical logic and formal verification is employed in order to ensure correct behavior of the control algorithm. This paper presents What You Prove Is What You Execute (WYPIWYE) compilation strategy for a Globally Asynchronous Locally Synchronous (GALS) programming language called Safey-Critical SystemJ. SC-SystemJ is a safety-critical subset of the SystemJ language. A formal big-step transition semantics of SC-SystemJ is developed for compiling SC-SystemJ programs into propositional Linear Temporal Logic formulas. These LTL formulas are then converted into a network of Mealy automata using a novel and efficient compilation algorithm. The resultant Mealy automata have a straightforward syntactic translation into Promela code. The resultant Promela models can be used for verifying correctness properties via the SPIN model-checker. Finally there is a single translation procedure to compile both: Promela and C/Java code for execution, which satisfies the De-Bruijn index, i.e. this final translation step is simple enough that is can be manually verified.     

Model checking adaptive service compositions

We present a logic-based verification framework for multilevel security and transactional correctness of service oriented architectures. The framework is targeted at the analysis of data confidentiality, enforced by non-interference, and of service responsiveness, captured by a notion of compliance that implies deadlock and livelock freedom. We isolate a class of modal μ-calculus formulae, interpreted over service configurations, that characterise configurations satisfying the properties of interest. We then investigate an adaptation technique based on the use of coercion filters to block any action that might potentially break security or transactional correctness. Based on the above, we devise a model checking algorithm for adaptive service compositions which automatically synthesises the maximal (most expressive/permissive) filter enforcing the desired security and correctness properties.     

Query-based verification of qualitative trends and oscillations in biochemical systems

We investigate the application of query-based verification to the analysis of behavioural trends of stochastic models of biochemical systems. We derive temporal logic properties which address specific behavioural questions, such as the likelihood for a species to reach a peak/deadlock state, or to exhibit monotonic/oscillatory trends. We introduce a specific modelling convention through which stochastic models of biochemical systems are made suitable to verification of the behavioural queries we define. Based on the queries we identify, we define a classification procedure which, given a stochastic model, allows for identifying meaningful qualitative behavioural trends. We illustrate the proposed query-based classification on a number of simple abstract models of biochemical systems.     

一种软件复杂性度量系统的设计与实现

本文结合软件复杂性度量的多种算法,对我们研制开发的一个软件复杂性度量系统,进行了详细介绍,并将系统与已有的各种度量工具进行了分析比较。     

基于经典逻辑的安全协议模型检测方法

本文分别以安全协议模型检测器SATMC和ProVerif为例,介绍了基于经典逻辑的安全协议模型检测两种方法:SAT方法和归结方法,并简要地给出了我们设计实现的基于SAT方法的安全协议模型检测器JLU-PV.     

Automatic Verification of a Behavioural Subset of UML Statechart Diagrams Using the SPIN Model-checker

Statechart Diagrams provide a graphical notation for describing dynamic aspects of system behaviour within the Unified Modelling Language (UML). In this paper we present a translation from a subset of UML Statechart Diagrams - covering essential aspects of both concurrent behaviour, like sequentialisation, parallelism, non-determinism and priority, and state refinement - into PROMELA, the specification language of the SPIN model checker. SPIN is one of the most advanced analysis and verification tools available nowadays. Our translation allows for the automatic verification of UML Statechart Diagrams. The translation is simple, proven correct, and promising in terms of state space representation efficiency. Received September 1999 / Accepted in revised form February 2000     

基于特定范围的关键字的快速排序算法

本文给出了一种对关键字在特定范围内的数据记录不用进行数据的比较交换的快速排序算法、算法思想、算法描述、时间复杂度及空间复杂度分析,并用C＋＋语言编写程序进行算法比较。结果表明：在关键字范围远远小于记录数的情况下,此算法的时间复杂度仅为O（n）,并且明显优于其他排序算法。     

排序算法探讨

通过对多种排序方法的比较与评价,提出多种改进的思路,形成改进型的排序算法。这些改进型的算法通过减少比较次数或交换次数,从而进一步改进平均情况下算法的时间性能。     

Model Checking of Time Petri Nets Using the State Class Timed Automaton

In this paper, we propose a method for building the state class graph of a bounded time Petri net (TPN) as a timed automaton (TA), which we call the state class timed automaton. We consider bounded TPN, whose underlying net is not necessarily bounded. We prove that our translation preserves the behavioral semantics of the TPN (the initial TPN and the obtained TA are proved timed-bisimilar). It allows us to check real-time properties on TPN by using the state class TA. This can be done efficiently thanks to a reduction of the number of clocks. We have implemented the method, and give some experimental results illustrating the efficiency of the translation algorithm in terms of number of clocks. Using the state class TA, we also give a framework for expressing and efficiently verifying TCTL properties on the initial TPN.