scholarly journals Diagonal Constraints in Timed Automata: Forward Analysis of Timed Systems

2005 ◽  
pp. 112-126 ◽  
Author(s):  
Patricia Bouyer ◽  
François Laroussinie ◽  
Pierre-Alain Reynier
Keyword(s):  
Timed Automata ◽  
Timed Systems ◽  
Forward Analysis

scholarly journals AN INVERSE METHOD FOR PARAMETRIC TIMED AUTOMATA

2009 ◽  
Vol 20 (05) ◽  
pp. 819-836 ◽  
Author(s):  
ÉTIENNE ANDRÉ ◽  
THOMAS CHATAIN ◽  
LAURENT FRIBOURG ◽  
EMMANUELLE ENCRENAZ
Keyword(s):  
Inverse Method ◽  
Timed Automata ◽  
Communication Protocols ◽  
Asynchronous Circuits ◽  
Synthesis Methods ◽  
Timed Systems ◽  
Prototype Implementation ◽  
Two Parameter

We consider in this paper systems modeled by timed automata. The timing bounds involved in the action guards and location invariants of our timed automata are not constants, but parameters. Those parametric timed automata allow the modelling of various kinds of timed systems, e.g. communication protocols or asynchronous circuits. We will also assume that we are given an initial tuple π0 of values for the parameters, which corresponds to values for which the system is known to behave properly. Our goal is to compute a constraint K0 on the parameters, satisfied by π0, guaranteeing that, under any parameter valuation satisfying K0, the system behaves in the same manner: for any two parameter valuations satisfying K0, the behaviors of the timed automata are (time-abstract) equivalent, i.e., the traces of execution viewed as alternating sequences of actions and locations are identical. We present an algorithm InverseMethod that terminates in the case of acyclic models, and discuss how to extend it to the cyclic case. We also explain how to combine our method with classical synthesis methods which are based on the avoidance of a given set of bad states. A prototype implementation has been done, and various experiments are described.

scholarly journals Timed Automata May Cause Some Troubles

2002 ◽  
Vol 9 (35) ◽  
Author(s):  
Patricia Bouyer
Keyword(s):  
Data Structures ◽  
General Framework ◽  
Timed Automata ◽  
Exact Computation ◽  
Analysis Algorithm ◽  
Forward Analysis

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 does not support a natural implementation and, in practice, 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.<br /> <br />In this paper, we study in details this widening operator and the forward analysis algorithm that uses it. 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, that uses such a widening operator, and which is correct. This goes really against what one could think. We then study in details 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.

scholarly journals Verification and Parameter Synthesis for Real-Time Programs using Refinement of Trace Abstraction*

2021 ◽  
Vol 178 (1-2) ◽  
pp. 31-57
Author(s):  
Franck Cassez ◽  
Peter Gjøl Jensen ◽  
Kim Guldstrand Larsen
Keyword(s):  
Real Time ◽  
State Of The Art ◽  
Timed Automata ◽  
Robustness Analysis ◽  
Hybrid Automata ◽  
Timed Systems ◽  
Current State ◽  
Parameter Synthesis ◽  
Series Of Experiments ◽  
Time Systems

We address the safety verification and synthesis problems for real-time systems. We introduce real-time programs that are made of instructions that can perform assignments to discrete and real-valued variables. They are general enough to capture interesting classes of timed systems such as timed automata, stopwatch automata, time(d) Petri nets and hybrid automata. We propose a semi-algorithm using refinement of trace abstractions to solve both the reachability verification problem and the parameter synthesis problem for real-time programs. All of the algorithms proposed have been implemented and we have conducted a series of experiments, comparing the performance of our new approach to state-of-the-art tools in classical reachability, robustness analysis and parameter synthesis for timed systems. We show that our new method provides solutions to problems which are unsolvable by the current state-of-the-art tools.

scholarly journals On Memory-Block Traversal Problems in Model Checking Timed Systems

2000 ◽  
Vol 7 (3) ◽  
Author(s):  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
State Space ◽  
Operating Systems ◽  
Memory Management ◽  
Timed Automata ◽  
Model Checker ◽  
Timed Systems ◽  
Memory Block ◽  
Start Up

A major problem in model-checking timed systems is the<br />huge memory requirement. In this paper, we study the memory-block<br />traversal problems of using standard operating systems in exploring the<br />state-space of timed automata. We report a case study which demonstrates<br />that deallocating memory blocks (i.e. memory-block traversal)<br />using standard memory management routines is extremely time-consuming.<br />The phenomenon is demonstrated in a number of experiments by<br />installing the Uppaal tool on Windows95, SunOS 5 and Linux. It seems<br />that the problem should be solved by implementing a memory manager<br />for the model-checker, which is a troublesome task as it is involved in<br />the underlining hardware and operating system. We present an alternative<br />technique that allows the model-checker to control the memory-block<br />traversal strategies of the operating systems without implementing<br />an independent memory manager. The technique is implemented in the<br />Uppaal model-checker. Our experiments demonstrate that it results in<br />significant improvement on the performance of Uppaal. For example, it<br />reduces the memory deallocation time in checking a start-up synchronisation<br />protocol on Linux from 7 days to about 1 hour. We show that the<br />technique can also be applied in speeding up re-traversals of explored<br />state-space.

Sign in / Sign up

Export Citation Format

Share Document