In this paper we introduce a framework for computing upper bounds yet accurate WCET for hardware platforms with caches and pipelines. The methodology we propose consists of 3 steps: 1) given a program to analyse, compute an equivalent (WCET-wise) abstract program; 2) build a timed game by composing this abstract program with a network of timed automata modeling the architecture; and 3) compute the WCET as the optimal time to reach a winning state in this game. We demonstrate the applicability of our framework on standard benchmarks for an ARM9 processor with instruction and data caches, and compute the WCET with UPPAAL-TiGA. We also show that this framework can easily be extended to take into account dynamic changes in the speed of the processor during program execution.
In this paper, we show how to apply recent tools for the automatic synthesis of robust and near-optimal controllers for a real industrial case study. We show how to use three different classes of models and their supporting existing tools, TiGA for synthesis, PHAVer for verification, and Simulink for simulation, in a complementary way. We believe that this case study shows that our tools have reached a level of maturity that allows us to tackle interesting and relevant industrial control problems.
In this paper, we review some recent results on the efficient synthesis of controllers for timed systems. We first recall the basics of controller synthesis for timed games and then present an efficient on-the-fly algorithm for reachability games and its extension to partially observable timed games.
In this paper we consider the problem of controller synthesis for timed games under imperfect information. Novel to our approach is the requirements to strategies: they should be based on a finite collection of observations and must be stuttering invariant in the sense that repeated identical observations will not change the strategy. We provide a constructive transformation to equivalent finite games with perfect information, giving decidability as well as allowing for an efficient on-the-fly forward algorithm. We report on application of an initial experimental implementation.
In this paper, we propose a first efficient on-the-fly algorithm for solving games based on timed game automata with respect to reachability and safety properties. The algorithm we propose is a symbolic extension of the on-the-fly algorithm suggested by Liu & Smolka [LS98] for linear-time model-checking of finite-state systems. Being on-the-fly, the symbolic algorithm may terminate long before having explored the entire state-space. Also the individual steps of the algorithm are carried out efficiently by the use of so-called zones as the underlying data structure. Various optimizations of the basic symbolic algorithm are proposed as well as methods for obtaining time-optimal winning strategies (for reachability games). Extensive evaluation of an experimental implementation of the algorithm yields very encouraging performance results.
Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost. Under stronger conditions (strictness of constraints) we prove that in case an optimal strategy exists, we can compute a state-based winning optimal strategy.
Priced timed (game) automata extend timed (game) automata with costs on both locations and transitions. The problem of synthesizing an optimal winning strategy for a priced timed game under some hypotheses has been shown decidable in [6]. In this paper, we present an algorithm for computing the optimal cost and for synthesizing an optimal strategy in case there exists one. We also describe the implementation of this algorithm with the tool HyTech and present an example.
In the literature, we find several formulations of the control problem for timed and hybrid systems. We argue that formulations where a controller can cause an action at any point in dense (rational or real) time are problematic, by presenting an example where the controller must act faster and faster, yet causes no Zeno effects (say, the control actions are at times 0,(1)/(2),1,1(1)/(4),2,2(1)/(8),3,3(1)/(16),...). Such a controller is, of course, not implementable in software. Such controllers are avoided by formulations where the controller can cause actions only at discrete (integer) points in time. While the resulting control problem is well-understood if the time unit, or ``sampling rate'' of the controller, is fixed a priori, we define a novel, stronger formulation: the discrete-time control problem with unknown sampling rate asks if a sampling controller exists for some sampling rate. We prove that this problem is undecidable even in the special case of timed automata.
In this book Chapter we address the problem of controller synthesis for timed systems. By timed systems we refer to systems which are subject to quantitative (hard) real-time constraints. We assume the reader is familiar with the basics of Timed Automata theory, or has read Chapter 1 and Chapter 2 in this book.
Ce chapitre traite de la synthèse de contrôleurs pour les systèmes temporisés. Par systèmes temporisés nous entendons les systèmes dans lesquels des contraintes de temps quantitatives sont spécifées. Les notions de base que nous utilisons dans ce chapitre s'appuient sur les concepts introduits dans les chapitre 3 et chapitre 4 ; la lecture de ces chapitres est donc recommandée au lecteur qui ne connaitrait pas les fondements des automates temporisés.
Cet article est une introduction au contrôle des systèmes modélisés par des automates temporisés. Nous définissons les notions de base du contrôle vu comme un jeu: stratégie, objectif de contrôle, états gagnants. On s'intéresse ensuite aux opérateurs de base permettant de résoudre les jeux temporisés. Nous considérons le cas des jeux de sûreté pour lesquels nous donnons un exemple complet de calcul de contrôleur. Nous abordons ensuite la notion importante d'implémentabilité des contrôleurs. Deux points de vue sont proposés: l'un syntaxique, qui consiste à décrire la plate-forme cible pour l'implémentation par des automates temporisés; l'autre sémantique, qui considère une sémantique implémentable des automates temporisés.
Priced timed (game) automata extends timed (game) automata with costs on both locations and transitions. In this paper we focus on reachability games for priced timed game automata and prove that the optimal cost for winning such a game is computable under conditions concerning the non-zenoness of cost. Under stronger conditions (strictness of constraints) we prove in addition that it is decidable whether there is an optimal strategy in which case an optimal strategy can be computed. Our results extend previous decidability result which requires the underlying game automata to be acyclic. Finally, our results are encoded in a first prototype in HyTech which is applied on a small case-study.
In this paper we give a symbolic concurrent semantics for network of timed automata (NTA) in terms of extended symbolic nets. Extended symbolic nets are standard occurrence nets extended with read arcs and symbolic constraints on places and transitions. We prove that there is a complete finite prefix for any NTA that contains at least the information of the simulation graph of the NTA but keep explicit the notions of concurrency and causality of the network.
In this paper we define and study the class of stopwatch automata which are timed automata augmented with stopwatches and unobservable behaviour. In particular, we investigate the expressive power of this class of automata, and show as a main result that any finite or infinite timed language accepted by a linear hybrid automaton is also acceptable by a stopwatch automaton. The consequences of this result are two-fold: firstly, it shows that the seemingly minor upgrade from timed automata to stopwatch automata immediately yields the full expressive power of linear hybrid automata. Secondly, reachability analysis of linear hybrid automata may effectively be reduced to reachability analysis of stopwatch automata. This, in turn, may be carried out using an easy (over-approximating) extension of the efficient reachability analysis for timed automata to stopwatch automata. We report on preliminary experiments on analyzing translations of linear hybrid automata using a stopwatch-extension of the real-time verification tool UPPAAL.
In this paper we give a symbolic concurrent semantics for network of timed automata (NTA) in terms of extended symbolic nets. Symbolic nets are standard occurrence nets extended with read arcs and symbolic constraints on places and transitions. We prove that there is a complete finite prefix for any NTA that contains at least the information of the simulation graph of the NTA but keep explicit the notions of concurrency and causality of the network.
In this paper, a timed modal logic Lc is presented for the specification and verification of real-time systems. Several important results for Lc are discussed. First we address the model checking problem and we show that it is an EXPTIME-complete problem. Secondly we consider expressiveness and we explain how to express strong timed bisimilarity and how to build characteristic formulas for timed automata. We also propose a compositional algorithm for Lc model checking. Finally we consider several control problems for which Lc can be used to check controllability.
In this paper we use the timed modal logic Lν to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (Lc) of the logic Lnu with a new modality. More precisely we define a fragment of Lν, namely Lνd, such that any control objective of Lνd can be translated into a Lc formula that holds for the plant if and only if there is a controller that can enforce the control objective. We also show that the new modality of Lc strictly increases the expressive power of Lν while model-checking of Lc remains EXPTIME-complete.
In this paper we use the timed modal logic Lν to specify control objectives for timed plants. We show that the control problem for a large class of objectives can be reduced to a model-checking problem for an extension (Lc) of the logic Lnu with a new modality. More precisely we define a fragment of Lν, namely Lνd, such that any control objective of Lνd can be translated into a Lc formula that holds for the plant if and only if there is a controller that can enforce the control objective. We also show that the new modality of Lc strictly increases the expressive power of Lν while model-checking of Lc remains EXPTIME-complete.
In this paper we present a semi-algorithm to do compositional model-checking for hybrid systems. We first define a modal logic Lν which is expressively complete for linear hybrid automata. We then show that it is possible to extend the result on compositional model-checking for parallel compositions of finite automata and networks of timed automata to linear hybrid automata. Finally we present some results obtained with an extension of the tool CMC to handle a subclass of hybrid automata (the stopwatch automata).
In this paper we extend the work on dynamic observers for fault diagnosis to timed automata. We study sensor minimization problems with static observers and then address the problem of computing the most permissive dynamic observer for a system given by a timed automaton.
In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterization of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterizes diagnosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. Finally we address the codiagnosis problem for TA under bounded resources and show it is 2EXPTIME-complete.
In this paper we study the fault codiagnosis problem for discrete event systems given by finite automata (FA) and timed systems given by timed automata (TA). We provide a uniform characterization of codiagnosability for FA and TA which extends the necessary and sufficient condition that characterizes diagnosability. We also settle the complexity of the codiagnosability problems both for FA and TA and show that codiagnosability is PSPACE-complete in both cases. For FA this improves on the previously known bound (EXPTIME) and for TA it is a new result. Finally we address the codiagnosis problem for TA under bounded resources and show it is 2EXPTIME-complete.
We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of fixed static observers, where the set of observable events is fixed and does not change during execution of the system. In this paper, we consider static observers where the set of observable events is not fixed, but needs to be optimized (e.g., minimized in size). We also consider dynamic observers, where the observer can ``switch'' sensors on or off, thus dynamically changing the set of events it wishes to observe. It is known that checking diagnosability (i.e., whether a given observer is capable of identifying faults) can be solved in polynomial time for static observers, and we show that the same is true for dynamic ones. On the other hand, minimizing the number of (static) observable events required to achieve diagnosability is NP-complete. We show that this is true also in the case of mask-based observation, where some events are observable but not distinguishable. For dynamic observers' synthesis, we prove that a most permissive finite-state observer can be computed in doubly exponential time, using a game-theoretic approach. We further investigate optimization problems for dynamic observers and define a notion of cost of an observer. We show how to compute an optimal observer using results on mean-payoff games by Zwick and Paterson.
In this paper we review algorithms for checking diagnosability of discrete-event systems and timed automata. We point out that the diagnosability problems in both cases reduce to the emptiness problem for (timed) Büchi automata. Moreover, it is known that, checking whether a discrete-event system is diagnosable, can also be reduced to checking bounded diagnosability. We establish a similar result for timed automata. We also provide a synthesis of the complexity results for the different fault diagnosis problems.
In this paper, we review some recent results about the use of dynamic observers for fault diagnosis of discrete event systems. Dynamic observers can switch sensors on or off, thus dynamically changing the set of events they wish to observe. We study the dynamic diagnoser synthesis problem and some related optimization problems.
We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists of synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider static as well as dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe.
Fault diagnosis consists in synthesizing a diagnoser that observes a given plant through a set of observable events, and identifies faults which are not observable as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during exe- cution of the system. In this paper, we consider dynamic observers, where the observer can switch sensors on or off, thus dynamically changing the set of events it wishes to observe. We define a notion of cost for such dynamic observers and show that (i) the cost of a given dynamic observer can be computed and (ii) an optimal dynamic observer can be synthesized.
We study the monitoring and fault-diagnosis problems for dense-time real-time systems, where observers (monitors and diagnosers) have access to digital rather than analog clocks. Analog clocks are infinitely-precise, thus, not implementable. We show how, given a specification modeled as a timed automaton and a timed automaton model of the digital clock, a sound and optimal (i.e., as precise as possible) digital-clock monitor can be synthesized. We also show how, given plant and digital clock modeled as timed automata, we can check existence of a digital-clock diagnoser and, if one exists, how to synthesize it. Finally, we consider the problem of existence of digital-clock diag- nosers where the digital clock is unknown. We show that there are cases where a digital clock, no matter how precise, does not exist, even though the system is diagnosable with analog clocks. Finally, we provide a sufficient condition for digital-clock diagnosability. check whether the observed behavior satisfies the specification. This is the objective of the observer, which in this case is called a monitor. Our goal is to synthesize a monitor automatically from the specification. In the fault-diagnosis problem, we have a model of the system, for instance, in the form of an (untimed or timed) automaton. We also know that the system may produce some faults. However, these faults are not directly observable, thus, their occurrence must be deduced from other observations (this can be seen as a grey-box setting). The objective of the observer, which in this case is called a diagnoser, is to detect whether a fault occurred or not, and this as soon as possible after the fault happened. In this case, before we attempt to synthesize a diagnoser, we must first check existence of a diagnoser, called diagnosability. Indeed, a diagnoser may not exist in cases where the system
In this book Chapter, we review the main results pertaining to the problem of fault diagnosis of timed automata. Timed automata are introduced in Chapter 1 and Chapter 2 in this book, and the reader not familiar with this model is invited to read them first.
Dans ce chapitre nous donnons les principaux résultats concernant le diagnostic de fautes dans les systèmes temporisés. Le modèle de systèmes temporisés que nous prenons est celui des automates temporisés introduits dans les chapitre 3 et chapitre 4. Nous invitons le lecteur qui n'est pas familier avec ce modèle à consulter ces chapitres préalablement à la lecture de celui-ci.
We study sensor minimization problems in the context of fault diagnosis. Fault diagnosis consists in synthesizing a diagnoser that observes a given plant and identifies faults in the plant as soon as possible after their occurrence. Existing literature on this problem has considered the case of static observers, where the set of observable events does not change during execution of the system. In this paper, we consider static as well as dynamic observers, where the observer can ``switch'' sensors on or off, thus dynamically changing the set of events it wishes to observe. It is known that checking diagnosability (whether an observer capable of identifying faults exists) can be solved in polynomial time for static observers, and we show that the same is true for dynamic ones. On the other hand, minimizing the number of (static) observable events required to achieve diagnosability is NP-complete. We show that this is true also in the case of mask-based observation, where some events are observable but not distinguishable. For dynamic observers, we prove that a most permissive observer can be computed in doubly exponential time, using a game-theoretic approach. We further investigate optimization problems for dynamic observers and define a notion of cost of an observer. Finally we show how to compute an optimal observer.
The paper considers the complexity of verifying that a finite state system satisfies a number of definitions of information flow security. The systems model considered is one in which agents operate synchronously with awareness of the global clock. This enables timing based attacks to be captured, whereas previous work on this topic has dealt primarily with asynchronous systems. Versions of the notions of nondeducibility on inputs, nondeducibility on strategies, and an unwinding based notion are formulated for this model. All three notions are shown to be decidable, and their computational complexity is characterised.
In this paper, we focus on the synthesis of secure timed systems which are given by timed automata. The security property that the system must satisfy is a non-interference property. Various notions of non-interference have been defined in the literature, and in this paper we focus on Strong Non-deterministic Non-Interference (SNNI) and we study the two following problems: (1) check whether it is possible to enforce a system to be SNNI; if yes (2) compute a sub-system which is SNNI.
In this paper, we address the problem of synthesizing opaque systems by selecting the set of observable events. We first investigate the case of static observability where the set of observable events is fixed a priori. In this context, we show that checking whether a system is opaque and computing an optimal static observer ensuring opacity are both PSPACE-complete problems. Next, we introduce dynamic partial observability where the set of observable events can change over time. We show how to check that a system is opaque a dynamic observer and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic observers under which S is opaque. Our main result is that the synthesis problem can be solved in EXPTIME.
In this paper we extend the notion of opacity, defined for discrete-event systems, to dense-time systems. We define the timed opacity problem for timed automata and study its algorithmic status. We show that for the very restrictive class of Event Recording Timed Automata, the opacity problem is already undecidable leaving no hope for an algorithmic solution to the opacity problem in dense-time.
In this paper, we focus on distributed systems sub ject to security issues. Such systems are usually composed of two entities: a high level user and a low level user that can both do some actions. The security properties we consider are non-interference properties. A system is non-interferent if the low level user cannot deduce any information by playing its low level actions. Various notions of non-interference have been defined in the literature, and in this paper we focus on two of them: one trace-based property (SNNI) and another bisimulation-based property (BSNNI). For these properties we study the problems of synthesis of a high level user so that the system is non-interferent. We prove that a most permissive high level user can be computed when one exists.
In this paper, we focus on the synthesis of secure systems. We assume the system is composed of two users, the low level and the high level users. The security property the system must satisfy is a non-interference property. A system is non-interferent if the low level user cannot deduce any information about the system by playing its low level actions. Various notions of non-interference have been defined in the literature, and in this paper we consider the most popular ones: trace-based non-interference (SNNI) and (bi)simulation-based non-interference (CSNNI and BSNNI). For each of these notions, we study the corresponding synthesis problem, build a controller the controlled system is non-interferent.
In this paper, we address the problem of synthesizing opaque systems. A secret predicate S over the runs of a system G is opaque to an external user having partial observability over G, if s/he can never infer from the observation of a run of G that the run belongs to S. We first investigate the case of static partial observability where the set of events the user can observe is fixed a priori. In this context, we show that checking whether a system is opaque is PSPACE-complete, which implies that computing an optimal static observer ensuring opacity is also a PSPACE-complete problem. Next, we introduce dynamic partial observability where the set of events the user can observe changes over time. We show how to check that a system is opaque to a dynamic observer and also address the corresponding synthesis problem: given a system G and secret states S, compute the set of dynamic observers under which S is opaque. Our main result is that the set of such observers can be finitely represented and can be computed in EXPTIME.
In this paper, we compare Timed Automata (TA) and Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is strictly included in the class of TA. It is thus natural to try and identify the subclass TAwtb of TA equivalent to some TPN for the weak timed bisimulation relation. We give a characterization of this subclass and we show that the membership problem and the reachability problem for TAwtb are PSPACE-complete. Furthermore we show that for a TA in TAwtb with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.
In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioral semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical appli- cations of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analyzing timed automata (like Kronos, Uppaal or Cmc) to analyze TPNs. In this paper we describe the new feature of the tool Romeo that implements our translation of TPNs in the Uppaal input format. We also report on experiments carried out on various examples and compare the result of our method to state-of-the-art tool for analyzing TPNs.
In this paper we consider the model of Time Petri Nets (TPN) where time is associated with transitions. We also consider Timed Automata (TA) as defined by Alur & Dill, and compare the expressive- ness of the two models w.r.t. timed language acceptance and (weak) timed bisimilarity. We first prove that there exists a TA A s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to A. We then propose a structural translation from TA to (1-safe) TPNs preserv- ing timed language acceptance. Further on, we prove that the previous (slightly extended) translation also preserves weak timed bisimilarity for a syntactical subclass TAsyn(<=,>=) of TA. For the theory of TPNs, the consequences are: 1) TA, bounded TPNs and 1-safe TPNs are equally expressive w.r.t. timed language acceptance; 2) TA are strictly more expressive than bounded TPNs w.r.t. timed bisimilarity; 3) The subclass TAsyn(<=,>=), bounded and 1-safe TPNs ''`a la Merlin'' are equally ex- pressive w.r.t. timed bisimilarity.
In this paper, we compare Timed Automata (TA) with Time Petri Nets (TPN) with respect to weak timed bisimilarity. It is already known that the class of bounded TPNs is included in the class of TA. It is thus natural to try and identify the (strict) subclass of TA that is equivalent to TPN for the weak time bisimulation relation. We give a characterisation of this subclass and we show that the membership problem and the reachability problem for are PSPACE-complete. Furthermore we show that for a TA in with integer constants, an equivalent TPN can be built with integer bounds but with a size exponential w.r.t. the original model. Surprisingly, using rational bounds yields a TPN whose size is linear.
In this paper we study the model of Time Petri Nets (TPNs) where a time interval is associated with the firing of a transition, but we extend it by considering general intervals rather than closed ones. A key feature of timed models is the memory policy, i.e. which timing informations are kept when a transition is fired. The original model selects an intermediate semantics where the transitions disabled after consuming the tokens, as well as the firing transition, are reinitialised. However this semantics is not appropriate for some applications. So we consider here two alternative semantics: the atomic and the persistent atomic ones. First we present relevant patterns of discrete event systems which show the interest of these semantics. Then we compare the expressiveness of the three semantics w.r.t. the weak time bisimilarity establishing inclusion results in the general case. Furthermore we show that some inclusions are strict with unrestricted intervals even when nets are bounded. Then we focus on bounded TPNs with upper-closed intervals and we prove that the semantics are equivalent. Finally taking into account both the practical and the theoretical issues, we conclude that persistent atomic semantics should be preferred.
In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioural semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical applications of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analysing timed automata (like KRONOS or UPPAAL or CMC) to analyse TPNs.
In this chapter we introduce a formalism, Time Petri Nets (TPNs), to model real-time systems. We compare it with another well-known formalism, Timed Automata (TA), used for specifying timed systems. We precisely define the semantics of TPNs and TA and compare them according to two criteria: the languages (or set of behaviours) then can generate, and the trees (or branching behaviours) they can generate. We show that every TPN can be translated into an equivalent TA. Then, we introduce a real-time logic to specify properties of real-time systems. We show how to check that a given TPN satisfies a property written in this logic. For this we use our translationThis translation preserves the properties of this logic. from TPNs to TA and check the property on the equivalent TA. Finally we briefly report on experiments for checking real-time properties of TPNs using this framework.
Dans cet article, nous considérons les réseaux de Petri t-temporels (RdPT) c'est à dire pour lesquels le temps est associé aux transitions sous la forme d'un interval. Nous en donnons une sémantique formelle en terme de systèmes de transitions temporisés. Nous proposons ensuite une traduction structurelle des RdPTs en un produit synchronisé d'automates temporisés (ATs) qui préserve la sémantique comportementale (bisimilarité temporelle) des RdPTs. Les conséquences théoriques de ce résultat sont: i) les problémes d'accessibilité et plus généralement de model-checking de TCTL sont décidables pour les RdPTs bornés; ii) il est possible d'étendre les RdPTs en considérant des contraintes temporelles strictes sur les transitions en préservant les résultats décrits plus haut en i). D'un point de vue pratique, les conséquences sont doubles: i) on peut spécifier un système à l'aide de RdPTs et d'automates temporisés et en donner une sémantique facilement; ii) les outils disponibles pour l'analyse des automates temporisés (comme KRONOS ou UPPAAL ou CMC) peuvent être utilisés pour la vérification de RdPTs.
In this paper we consider the model of Time Petri Nets (TPN) ``à la Merlin'' where time is associated with transitions, but we extend it with open intervals to specify the firing intervals of the transitions. We also consider Timed Automata (TA) as defined by Alur & Dill, and compare the expressiveness of the two models w.r.t. timed language acceptance and (weak) timed bisimilarity. We first prove the following results: 1) bounded TPNs and TA are equally expressive w.r.t. timed language acceptance; 2) there exists a TA A s.t. there is no TPN (even unbounded) that is (weakly) timed bisimilar to A. Because of 2) above, it is natural to try and identify the (strict) subclass of TA that is equivalent to TPN w.r.t. weak timed bisimilarity. Thus we give some further results: 1) we characterize the subclass TA- of TA that is equivalent to the original model of TPN as defined by Merlin, restricted to closed intervals, 2) we show that the associated membership problem for TA- is PSPACE-complete and 3) we prove that the reachability problem for TA- is also PSPACE-complete.
In this paper, we consider Time Petri Nets (TPN) where time is associated with transitions. We give a formal semantics for TPNs in terms of Timed Transition Systems. Then, we propose a translation from TPNs to Timed Automata (TA) that preserves the behavioural semantics (timed bisimilarity) of the TPNs. For the theory of TPNs this result is two-fold: i) reachability problems and more generally TCTL model-checking are decidable for bounded TPNs; ii) allowing strict time constraints on transitions for TPNs preserves the results described in i). The practical applications of the translation are: i) one can specify a system using both TPNs and Timed Automata and a precise semantics is given to the composition; ii) one can use existing tools for analysing timed automata (like KRONOS or UPPAAL or CMC) to analyse TPNs.
The aim of the paper is to revisit the model of Biological Regulatory Networks (BRN) which was proposed by René Thomas to model the interactions between a set of genes. We give a formal semantics for BRN in terms of transition systems which formalizes the evolution rules given by René Thomas. Then we show how to use this model to find interesting properties of a BRN like the set of stable states, cycles etc using tools for analyzing transition systems.
In this paper we present a timed extension of the AltaRica formalism. Following previous works, we first extend the semantics of AltaRica with time and define timed components and timed nodes. Moreover we lift the priority features of AltaRica to the timed case. We obtain a timed version of AltaRica, called Timed AltaRica. Finally we give a translation of a Timed AltaRica specification into a usual timed automaton. These are the semantic foundations of a high-level hierarchical language for the specification of timed systems.
We are concerned in this paper with the verification of reactive systems with event memorization. The reactive systems are specified with an asynchronous reactive language Electre the main feature of which is the capability of memorizing occurrences of events in order to process them later. This memory capability is quite interesting for specifying reactive systems but leads to a verification model with a dramatically large number of states (due to the stored occurrences of events). In this paper, we show that partial-order methods can be applied successfuly for verification purposes on our model of reactive programs with event memorization. The main points of our work are two-fold: (1) we show that the independance relation which is a key point for applying partial-order methods can be extracted automatically from an Electre program; (2) the partial-order technique turns out to be very efficient and may lead to a drastic reduction in the number of states of the model as demonstrated by a real-life industrial case study.
We present in this paper some new language features and constructs, that allow the joint synchronous/asynchronous programming of reactive applications, as well as their formal verification. We show that reactive applications may be dealt with from two points of view. First, from the chronological point of view, i.e., when reactions are instantaneous, generated by event occurrences in discrete time. Second, from the chronometrical point of view, when reactions have durations in dense time. This duality must be expressible in languages that allow a consistent programming of both synchronous and asynchronous features. The objective of mixing these dual approaches leads to model reactive systems by using hybrid systems, to deal simultaneously with both discrete and continuous phenomena. Furthermore, this must be followed by some verification of the application's properties, with respect to its behavioural and quantitative features. We analyze several existing frameworks that meet these requirements, and propose our own approach based on the language Electre.
GRAFCET is a graphical formalism derived from Petri Nets and widely used to program automation applications. So far, this formalism has not been equipped with a formal semantics: interpretation algorithms give the meaning of a GRAFCET description. Our purpose is to take advantage of the work carried out for reactive languages: these languages are given a precise behavioural semantics by means of finite-state machines; the behavioural model can then be checked for various properties. The work presented hereafter consists in equipping GRAFCET with a formal semantics to obtain a behavioural model (namely a timed automaton) that captures the metric aspect of time.
We present in this paper an operational semantics for the ELECTRE reactive language (Roux et al., 1992). This language is based on an asynchronous approach to real-time systems. First basic concepts and intuitive semantics are introduced. Then we give rules to model dynamic semantics of ELECTRE programs: this constitutes an operational semantics for the ELECTRE language. This operational semantics is used to define a model of execution for ELECTRE programs: transition system. In addition, we prove, using structural induction on the operational semantics, that this transition system is a finite state transition system. Eventually, we extend the previous transition system so as to handle multiple-storage events: it is important since the asynchronous ELECTRE language deals with multiple memorized occurrences of the events. This result gives a means of compiling the ELECTRE language into a finite-state machine.
Reactive Fiffo Systems (RFS) are used to model reactive systems which are able to memorize the events that cannot be processed when they occur. In this paper we investigate the decidability of verification problems for Embedded RFS which are RFS running under some environmental constraints. We show that almost all the usual verification problems are undecidable for the class of Periodically Embedded RFS with two memorizing events, whereas they become decidable for Regularly Embedded RFS with a single memorizing event. We then focus on Embedded Lossy RFS and we show in particular that for Regularly Embedded Lossy RFS the set of predecessors Pred* is upward closed and effectively computable.
This paper tackles the problem of model-checking SDL programs that use the save operator. Previous work on model-checking SDL programs with SPIN consisted in translating SDL into IF (using sdl2if) and finally IF to Promela (if2pml). However, the save operator of SDL is not handled by the (final) translator if2pml . We propose an extension of the if2pml tool that translates IF into Promela programs with save operators. We also add an abstraction method on buffer messages to if2pml allowing the user to gather some buffer messages into one abstract value. We use our extended version of if2pml to validate an Unmanned Underwater Vehicle (UUV) subsystem specified with SDL.
Our work intends to verify reactive systems with event memorization specified with the reactive language Electre. For this, we define a particular behavioral model for Electre programs, reactive FIFFO Automata (RFAs), which is close to Fifo Automata. Intuitively, a RFA is the model of a reactive system which may store event occurrences that must not be immediately taken into account. We show that, contrarily to lossy systems where the reachability set is rec ognizable but not effectively computable, (1) the reachability set of a RFA is recognizable, and (2) it is effectively computable. Moreover, we also study the relationships between RFAs and Finite Automata and we prove that (3) from a trace language point of view, inclusions between RFAs and Finite Automata are undecidable and (4) the linear temporal logic on states without the temporal operator next is decidable for RFAs, while on transitions is undecidable.
In this paper we present a timed extension of the AltaRica language, Timed AltaRica, and describe the architecture of a compiler from Timed AltaRica to timed automata. We present the features of the language, namely modularity, hierarchical modeling and reuse of components during the specification phase, on an avionics example. Then, we use the compiler from Timed AltaRica to Timed Automata to check some safety properties on the system.
In this work we present a timed extension of the AltaRica formalism. We extend the semantics of AltaRica to timed components and timed nodes. Moreover we also extend the priority mechanism of AltaRica to the timed case. Finally we give a translation of a Timed AltaRica specification into a usual timed automaton that can then be analysed by existing tools for checking properties of timed systems.
This short note explains how to install PHAVer (and the needed libraries) for a single user on Mac OS X running Leopard (10.5.6). It might also work for earlier versions (you can report to me in case of a successful install on earlier version).
Petite introduction aux automates finis et langages réguliers.
This LNCS Tutorials volume gathers the contributions of speakers who gave talks at the summer school MOVEP'00, held in Nantes, France in june 2000.