Timed CSP = Closed Timed Automata

We study the expressive power of an augmented version of Timed CSP and show that it is precisely equal to that of closed timed automatatimed automata with closed invariant and enabling clock constraints. We also show that this new version of Timed CSP is expressive enough to capture the most widely used specifications on timed systems as refinements between processes, and moreover that refinement checking is amenable to digitisation analysis. As a result, we are able to verify some of the most important timed specifications, including branching-time liveness properties such as timestop-freedom and constant availability, using the model checker FDR (a commercial product of Formal Systems (Europe) Ltd.).     

A theory of Orwellian specifications with NewThink

We introduce NewThink, a specification language designed specifically for real-time safety-critical systems. NewThink is a component of an overall Orwellian development method for safety-critical systems which consists of a specification language, a programming language and a set of sound decomposition rules. In this paper, we present the syntax and semantics of NewThink. We demonstrate a relationship between timed and static specifications, which potentially allows us to continue using techniques from the static case in the timed case. We also prove that our extension for real-time is conservative, which is very much in keeping with our Orwellian philosophy.     

Conformance Tests for Real-Time Systems with Timed Automata Specifications

A method is introduced for testing the conformance of implemented real-time systems to timed automata specifications. Uppaal timed automata are transformed into testable timed transition systems (TTTSs) using a test view. Fault hypotheses and a test generation algorithm for TTTSs are defined. Results of applying the method are presented. Received October 1999 / Accepted in revised form November 2000     

Grid automata and supervisory control of dense real-time discrete event systems

We present a generalization of the classical supervisory control theory for discrete event systems to a setting of dense real-time systems modeled by Alur and Dill timed automata. The main problem involved is that in general the state space of a timed automaton is (uncountably) infinite. The solution is to reduce the dense time transition system to an appropriate finite discrete subautomaton, the grid automaton, which contains enough information to deal with the timed supervisory control problem (TSCP). The plant and the specifications region graphs are sampled for a granularity defined in a way that each state has an outgoing transition labeled with the same time amount. We redefine the controllability concept in the context of grid automata, and we provide necessary and sufficient solvability conditions under which the optimal solution to centralized supervisory control problems in timed discrete event systems under full observation can be obtained. The enhanced setting admits subsystem composition and the concept of forcible event. A simple example illustrates how the new method can be used to solve the TSCP.     

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

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

Supervision localization of timed discrete-event systems

We study supervisor localization for real-time discrete-event systems (DES) in the Brandin–Wonham framework of timed supervisory control. We view a real-time DES as comprised of asynchronous agents which are coupled through imposed logical and temporal specifications; the essence of supervisor localization is the decomposition of monolithic (global) control action into local control strategies for these individual agents. This study extends our previous work on supervisor localization for untimed DES, in that monolithic timed control action typically includes not only disabling action as in the untimed case, but also “clock preempting” action which enforces prescribed temporal behavior. The latter action is executed by a class of special events, called “forcible” events; accordingly, we localize monolithic preemptive action with respect to these events. We demonstrate the new features of timed supervisor localization with a manufacturing cell case study and discuss a distributed control implementation.     

Automated test generation from timed automata

Testing is the most dominant validation activity used by industry today, and there is an urgent need for improving its effectiveness, both with respect to the time and resources for test generation and execution, and obtained test coverage. We present a new technique for automatic generation of real-time black-box conformance tests for non-deterministic systems from a determinizable class of timed automata specifications with a dense time interpretation. In contrast to other attempts, our tests are generated using a coarse equivalence class partitioning of the specification. To analyze the specification, to synthesize the timed tests, and to guarantee coverage with respect to a coverage criterion, we use the efficient symbolic techniques recently developed for model checking of real-time systems. Application of our prototype tool to a realistic specification shows promising results in terms of both the test suite size, and the time and space used for test generation.     

Timed Petri Nets in Hybrid Systems: Stability and Supervisory Control

In this paper, timed Petri nets are used to model and control hybrid systems. Petri nets are used instead of finite automata primarily because of the advantages they offer in dealing with concurrency and complexity issues. A brief overview of existing results on hybrid systems that are based on Petri nets is first presented. A class of timed Petri nets named programmable timed Petri nets (PTPN) is then used to model hybrid systems. Using the PTPN, the stability and supervisory control of hybrid systems are addressed and efficient algorithms are introduced. In particular, we present sufficient conditions for the uniform ultimate boundness of hybrid systems composed of multiple linear time invariant plants which are switched between using a logical rule described by a Petri net. This paper also examines the supervisory control of a hybrid system in which the continuous state is transfered to a region of the state space in a way that respects safety specifications on the plant's discrete and continuous dynamics.     

Automated analysis of the SCR-style requirements specifications

The SCR(Software Cost Reduction)requirements method is an effective method for specifying software system requirements.This paper presents a formal model analyzing SCR-style requirements.The analysis model mainly applies state translation rules,semantic computing rules and attributes to define formal semantics of a tabular notation in the SCR requirements method,and may be used to analyze requirements specifications to be specified by the SCR requirements method.Using a simple example,this paper introduces how to analyze consistency and completeness of requirements specifications.     

Supervisory control of real-time discrete-event systems usinglattice theory

The behaviour of timed discrete-event systems (DES's) can be described by sequences of event occurrence times. These sequences can be ordered to form a lattice. Since logical (untimed) DES behaviours described by regular languages also form a lattice, questions of controllability for timed DES's may be treated in much the same manner as they are for untimed systems. In this paper we establish conditions for the controllability of timed DES performance specification which are expressed as inequations on the lattice of sequences. These specifications may take the form of sets of acceptable event occurrence times, maximum or minimum occurrence times, or limits on the separation times between events. Optimal behaviours are found as extremal solutions to these inequations using fixed point results for lattices     

Dynamic Meta Modeling with time: Specifying the semantics of multimedia sequence diagrams

The Unified Modeling Langugage (UML) offers different diagram types to model the behavior of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time in behavioral models since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain.We have proposed Dynamic Meta Modeling (DMM), an approach based on graph transformation, as a means for specifying operational semantics of dynamic UML diagrams. In this article, we extend this approach to also account for time by extending the semantic domain to timed graph transformation. This enables us to define the operational semantics of UML diagrams with time specifications. As an example, we provide semantics for special sequence diagrams from the domain of multimedia application modeling.     

A control synthesis approach for time discrete event systems

In this paper, we introduce a control synthesis method for discrete event systems whose behavior is dependent on explicit values of time. Our goal is to control the occurrence dates of the controllable events so that the functioning of the system respects given specifications. The system to be controlled is modeled by a time Petri net. In a previous work we proposed a systematic method to build the timed automaton which models the exact behavior of a time Petri net. Furthermore, the forbidden behaviors of the system are modeled by forbidden timed automaton locations. This paper focuses on the control synthesis method, which consists in computing new firing conditions for the timed automaton transitions so that the forbidden locations are no longer reachable.     

Verification of real‐time systems design

The main objective of this paper is to present an approach to accomplish verification in the early design phases of a system, which allows us to make the system verification easier, specifically for those systems with timing restrictions. For this purpose we use RT‐UML sequence diagrams in the design phase and we translate these diagrams into timed automata for performing the verification by using model checking techniques. Specifically, we use the Object Management Group's UML Profile for Schedulability, Performance, and Time and from the specifications written using this profile we obtain the corresponding timed automata. The ‘RT‐UML Profile’ is used in conjunction with a very well‐known tool to perform validation and verification of the timing needs, namely, the UPPAAL tool, which is used to simulate and analyze the behaviour of real‐time dynamic systems described by timed automata. Copyright © 2009 John Wiley & Sons, Ltd.     

A New Class of Supervisors for Timed Discrete Event Systems Under Partial Observation

Brandin and Wonham have developed a supervisory control framework for timed discrete event systems (TDESs) in order to deal with not only logical specifications but also temporal specifications. Lin and Wonham have extended this framework to the partial observation case, and presented necessary and sufficient conditions for the existence of a nonblocking supervisor under partial observation. In this paper, we define a new class of supervisors for TDESs under partial observation. We then present necessary and sufficient conditions for the existence of a nonblocking supervisor defined in this paper. These existence conditions of our supervisor are weaker than those of Lin and Wonham's supervisor. Note, however, that the price that must be paid to weaken the existence conditions is the higher computational cost. Moreover, given a closed regular language, we study computation of a sublanguage that satisfies the existence conditions of our supervisor. We present an algorithm for computing such a sublanguage larger than the supremal closed, controllable, and normal sublanguage.     

一种基于场景的嵌入式软件设计方法

UML顺序图是一种常用的在软件开发早期阶段用来描述系统基于场景的需求规约的一种可视化建模语言。通过在UML顺序图中加入带时间区间标志的时间约束,得到时间顺序图模板TSDT（Timed Sequence Diagram Template）,用来建立嵌入式软件基于场景的需求规约模型。对消息传递自动机进行实时扩展,得到时间消息传递自动机TMPA（Timed Message Passing Automata）,TMPA以自动机的形式刻画了所建立的需求规约模型,为在需求阶段验证所建立的模型是否满足用户需求奠定了基础。     

Program Synthesis from Formal Requirements Specifications Using APTS

Formal specifications of software systems are extremely useful because they can be rigorously analyzed, verified, and validated, giving high confidence that the specification captures the desired behavior. To transfer this confidence to the actual source code implementation, a formal link is needed between the specification and the implementation. Generating the implementation directly from the specification provides one such link. A program transformation system such as Paige's APTS can be useful in developing a source code generator. This paper describes a case study in which APTS was used to produce code generators that construct C source code from a requirements specification in the SCR (Software Cost Reduction) tabular notation. In the study, two different code generation strategies were explored. The first strategy uses rewrite rules to transform the parse tree of an SCR specification into a parse tree for the corresponding C code. The second strategy associates a relation with each node of the specification parse tree. Each member of this relation acts as an attribute, holding the C code corresponding to the tree at the associated node; the root of the tree has the entire C program as its member of the relation. This paper describes the two code generators supported by APTS, how each was used to synthesize code for two example SCR requirements specifications, and what was learned about APTS from these implementations.     

Dynamic Meta Modeling with Time: Specifying the Semantics of Multimedia Sequence Diagrams

UML offers different diagram types to model behavior and dynamics of software systems. In some domains like embedded real-time systems or multimedia systems, it is necessary to include specifications of time since the correctness of these applications depends on the fulfillment of temporal requirements in addition to functional requirements. UML thus already incorporates language features to model time and temporal constraints. Such model elements must have an equivalent in the semantic domain. We have proposed Dynamic Meta Modeling (DMM) as a means for the specification of the formal operational semantics of UML models by applying graph transformation to the meta modeling of dynamic behavior. Within this paper, we extend this approach to also account for time by building on timed graph transformations. We apply these concepts to the domain of multimedia application modeling in which we adopt UML sequence diagrams. The DMM rules with time then specify an interpreter that can be used to analyze or test a model of multimedia sequence diagrams.     

Timed automata with urgent transitions

We propose an extension to the formalism of timed automata by allowing urgent transitions. An urgent transition is a transition which must be taken within a fixed time interval from its enabling time and it has higher priority than other non-urgent transitions enabled in the same state. We give a set of rules formally describing the behavior of urgent transitions and we show that, from a language theoretic point of view, the addition of urgency does not improve the expressive power of timed automata. From a specification point of view, the use of urgent transitions allows shorter and clear specifications of behaviors involving urgency and priority. We use timed automata with urgent transitions for specifying a multicast protocol for mobile computing.Received: 10 January 2003, Published online: 17 February 2004A first version of this paper appeared in [15]