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 Conformance Testing of Preemptive Real-Time Systems

2013 ◽  
Vol 4 (4) ◽  
pp. 1-26 ◽  
Author(s):  
Noureddine Adjir ◽  
Pierre de Saqui-Sannes ◽  
Kamel Mustapha Rahmouni
Keyword(s):  
Real Time ◽  
Test Generation ◽  
Conformance Testing ◽  
Black Box ◽  
Online Testing ◽  
Test Results ◽  
Real Time Systems ◽  
Test Specification ◽  
Partially Observable ◽  
Time Systems

The paper presents an approach for model-based black-box conformance testing of preemptive real-time systems using Labeled Prioritized Time Petri Nets with Stopwatches (LPrSwTPN). These models not only specify system/environment interactions and time constraints. They further enable modelling of suspend/resume operations in real-time systems. The test specification used to generate test primitives, to check the correctness of system responses and to draw test verdicts is an LPrSwTPN made up of two concurrent sub-nets that respectively specify the system under test and its environment. The algorithms used in the TINA model analyzer have been extended to support concurrent composed subnets. Relativized stopwatch timed input/output conformance serves as the notion of implementation correctness, essentially timed trace inclusion taking environment assumptions into account. Assuming the modelled systems are non deterministic and partially observable, the paper proposes a test generation and execution algorithm which is based on symbolic techniques and implements an online testing policy and outputs test results for the (part of the) selected environment.

scholarly journals IMITATOR 3: Synthesis of Timing Parameters Beyond Decidability

2021 ◽  
pp. 552-565
Author(s):  
Étienne André
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Robustness Analysis ◽  
Parametric Model ◽  
Timing Constraints ◽  
Real Time Systems ◽  
Model Checker ◽  
Time Systems ◽  
Timed Model Checking

AbstractReal-time systems are notoriously hard to verify due to nondeterminism, concurrency and timing constraints. When timing constants are uncertain (in early the design phase, or due to slight variations of the timing bounds), timed model checking techniques may not be satisfactory. In contrast, parametric timed model checking synthesizes timing values ensuring correctness. takes as input an extension of parametric timed automata (PTAs), a powerful formalism to formally verify critical real-time systems. extends PTAs with multi-rate clocks, global rational-valued variables and a set of additional useful features. We describe here the new features and algorithms offered by  3, that moved along the years from a simple prototype dedicated to robustness analysis to a standalone parametric model checker for timed systems.

scholarly journals UPPAAL—a Tool Suite for Automatic Verification of Real–Time Systems

1996 ◽  
Vol 3 (58) ◽  
Author(s):  
Johan Bengtsson ◽  
Kim G. Larsen ◽  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Real Time ◽  
Timed Automata ◽  
Automatic Verification ◽  
Graphical Interface ◽  
Real Time Systems ◽  
Model Checker ◽  
Current Version ◽  
Textual Representations ◽  
Liveness Properties ◽  
Time Systems

Uppaal is a tool suite for automatic verification of safety and<br />bounded liveness properties of real-time systems modeled as networks of<br />timed automata. It includes: a graphical interface that supports graphical<br />and textual representations of networks of timed automata, and automatic<br />transformation from graphical representations to textual format,<br />a compiler that transforms a certain class of linear hybrid systems to<br />networks of timed automata, and a model-checker which is implemented<br />based on constraint-solving techniques. Uppaal also supports diagnostic<br />model-checking providing diagnostic information in case verification of a<br />particular real-time systems fails.<br />The current version of Uppaal is available on the World Wide Web via<br />the Uppaal home page http://www.docs.uu.se/docs/rtmv/uppaal.

scholarly journals Reliability and performance optimization of pipelined real-time systems

2013 ◽  
Vol 73 (6) ◽  
pp. 851-865 ◽  
Author(s):  
Anne Benoit ◽  
Fanny Dufossé ◽  
Alain Girault ◽  
Yves Robert
Keyword(s):  
Real Time ◽  
Performance Optimization ◽  
Real Time Systems ◽  
And Performance ◽  
Time Systems

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 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.

Sign in / Sign up

Export Citation Format

Share Document