scholarly journals Automated Invariant Generation for the Verification of Real-Time Systems

10.29007/npn7 ◽  
2018 ◽  
Author(s):  
Bahareh Badban ◽  
Stefan Leue ◽  
Jan-Georg Smaus
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
Experimental Results ◽  
State Transitions ◽  
Real Time Systems ◽  
Prototype Implementation ◽  
Invariant Generation ◽  
Time Systems

We present an approach to automatically generating invariants for timed automata models. The CIPM algorithm that we propose first computes new invariants for timed automata control locations taking their originally defined invariants as well as the constrains on clock variables imposed by incoming state transitions into account. In doing so the CIPM algorithm also prunes idle transitions, which are transitions that can never be taken, from the automaton. We discsuss a prototype implementation of the CIPM algorithm as well as some initial experimental results.

MODELING AND ANALYSIS OF REAL-TIME SYSTEMS WITH MUTEX COMPONENTS

2012 ◽  
Vol 23 (04) ◽  
pp. 831-851 ◽  
Author(s):  
GUOQIANG LI ◽  
XIAOJUAN CAI ◽  
SHOJI YUEN
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
Expressive Power ◽  
Behavioral Model ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Modeling And Analysis ◽  
Compositional System ◽  
Time Systems ◽  
Timed Automaton

Timed automata are commonly recognized as a formal behavioral model for real-time systems. For compositional system design, parallel composition of timed automata as proposed by Larsen et al. [22] is useful. Although parallel composition provides a general method for system construction, in the low level behavior, components often behave sequentially by passing control via communication. This paper proposes a behavioral model, named controller automata, to combine timed automata by focusing on the control passing between components. In a controller automaton, to each state a timed automaton is assigned. A timed automaton at a state may be preempted by the control passing to another state by a global labeled transition. A controller automaton properly extends the expressive power because of the stack, but this can make the reachability problem undecidable. Given a strict partial order over states, we show that this problem can be avoided and a controller automaton can be faithfully translated into a timed automaton.

scholarly journals Online On-the-Fly Testing of Real-time Systems

2003 ◽  
Vol 10 (49) ◽  
Author(s):  
Marius Mikucionis ◽  
Kim G. Larsen ◽  
Brian Nielsen
Keyword(s):  
Real Time ◽  
Test Generation ◽  
Timed Automata ◽  
Online Testing ◽  
Real Time Systems ◽  
Model Checker ◽  
Test Specification ◽  
And Performance ◽  
Automata Network ◽  
Time Systems

In this paper we present a framework, an algorithm and a new tool for online testing of real-time systems based on symbolic techniques used in UPPAAL model checker. We extend UPPAAL timed automata network model to a test specification which is used to generate test primitives and to check the correctness of system responses including the timing aspects. We use timed trace inclusion as a conformance relation between system and specification to draw a test verdict. The test generation and execution algorithm is implemented as an extension to UPPAAL and experiments carried out to examine the correctness and performance of the tool. The experiment results are promising.

scholarly journals Time Petri Nets with Action Duration

2013 ◽  
Vol 4 (2) ◽  
pp. 62-83 ◽  
Author(s):  
N. Belala ◽  
D.E. Saїdouni ◽  
R. Boukharrou ◽  
A.C. Chaouche ◽  
A. Seraoui ◽  
...  
Keyword(s):  
Petri Nets ◽  
Real Time ◽  
Timed Automata ◽  
Operational Semantics ◽  
Time Interval ◽  
Timing Constraints ◽  
Time Petri Nets ◽  
Real Time Systems ◽  
High Level ◽  
Time Systems

The design of real-time systems needs a high-level specification model supporting at the same time timing constraints and actions duration. The authors introduce in this paper an extension of Petri Nets called Time Petri Nets with Action Duration (DTPN) where time is associated with transitions. In DTPN, the firing of transitions is bound to a time interval and transitions represent actions which have explicit durations. The authors give an operational semantics for DTPN in terms of Durational Action Timed Automata (DATA). DTPN considers both timing constraints and durations under a true-concurrency semantics with an aim of better expressing concurrent and parallel behaviours of real-time systems.

scholarly journals Automatic Synthesis of Real Time Systems

1994 ◽  
Vol 1 (45) ◽  
Author(s):  
Jørgen H. Andersen
Keyword(s):  
Real Time ◽  
Model Construction ◽  
Real Time Systems ◽  
Automatic Synthesis ◽  
Prototype Implementation ◽  
Construction Problem ◽  
Verification Tool ◽  
Logical Specification ◽  
Direct Model ◽  
Time Systems

This paper presents a method for automatically constructing real time systems directly from their specifications. The model-construction problem is considered for implicit specifications of the form: <br />(A_1 | . . . | A_n | X) sat S <br /> where S is a real time (logical) specification, A_1, ... , A_n are given (regular) timed agents and the problem is to decide whether there exists (and if possible exhibit) a real time agent X which when put in parallel with A_1, ..., A_n will yield a network satisfying S. The method presented proceeds in two steps: first, the implicit specification of X is transformed into an equivalent direct specification of X; second, a model for this direct specification is constructed (if possible) using a direct model construction algorithm. A prototype implementation of our method has been added to the real time verification tool EPSILON.

Sign in / Sign up

Export Citation Format

Share Document