scholarly journals Compositional Model Checking of Real Time Systems

1995 ◽  
Vol 2 (19) ◽  
Author(s):  
Francois Laroussinie ◽  
Kim G. Larsen
Keyword(s):  
Model Checking ◽  
Timed Automata ◽  
Parallel Composition ◽  
Combinatorial Explosion ◽  
Binary Decision ◽  
Practical Applications ◽  
Compositional Model ◽  
Finite State ◽  
Time Systems ◽  
Combined Technique

A major problem in applying model checking to finite-state systems<br />is the potential combinatorial explosion of the state space arising from<br />parallel composition. Solutions of this problem have been attempted for<br />practical applications using a variety of techniques. Recent work by Andersen<br />[And95] proposes a very promising compositional model checking<br />technique, which has experimentally been shown to improve results obtained<br />using Binary Decision Diagrams.<br />In this paper we make Andersen's technique applicable to systems described<br />by networks of timed automata. We present a quotient construction,<br />which allows timed automata components to be gradually moved from<br />the network expression into the specification. The intermediate specifications<br />are kept small using minimization heuristics suggested by Andersen.<br />The potential of the combined technique is demonstrated using a prototype<br />implemented in CAML.

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 Model Checking via Reachability Testing for Timed Automata

1997 ◽  
Vol 4 (29) ◽  
Author(s):  
Luca Aceto ◽  
Augusto Burgueno ◽  
Kim G. Larsen
Keyword(s):  
Model Checking ◽  
Timed Automata ◽  
Reachability Problem ◽  
Liveness Properties ◽  
Time Logic ◽  
Definition Of ◽  
Reachability Testing ◽  
Time Systems ◽  
Timed Automaton ◽  
Theoretical Side

In this paper we develop an approach to model-checking for timed automata via reachability testing. As our specification formalism, we consider a dense-time logic with clocks. This logic may be used to express safety and bounded liveness properties of real-time systems. We show how to automatically synthesize, for every logical formula phi, a so-called test automaton T_phi in such a way that checking whether a system S satisfies the property phi can be reduced to a reachability question over the system obtained by making T_phi interact with S. <br />The testable logic we consider is both of practical and theoretical interest. On the practical side, we have used the logic, and the associated approach to model-checking via reachability testing it supports, in the specification and verification in Uppaal of a collision avoidance protocol. On the theoretical side, we show that the logic is powerful enough to permit the definition of characteristic properties, with respect to a timed version of<br />the ready simulation preorder, for nodes of deterministic, tau-free timed automata. This allows one to compute behavioural relations via our model-checking technique, therefore effectively reducing the problem of checking the existence of a behavioural relation among states of a timed automaton to a reachability problem.

True Concurrency Semantics

2014 ◽  
Vol 5 (2) ◽  
pp. 22-42 ◽  
Author(s):  
Souad Guellati ◽  
Ilham Kitouni ◽  
Riad Matmat ◽  
Djamel-Eddine Saidouni
Keyword(s):  
Model Checking ◽  
Formal Verification ◽  
Timed Automata ◽  
Model Data ◽  
True Concurrency ◽  
New Class ◽  
Computation Tree ◽  
Interleaving Semantics ◽  
Finite State ◽  
Validation Technique

The model checking algorithms have been widely studied for timed automata, it's a validation technique for automatically verifying correctness properties of finite-state systems, which are based on interleaving semantics. Therefore the actions are assumed instantaneous. To overcome the hypothesis of temporal and structural atomicity of actions, we use the durational actions timed automata model (daTA). This model is based on the maximality semantics. Properties to be verified are expressed using the Timed Computation Tree Logic (TCTL). For dealing with formal verification, the Maximality-based Region Graph (MRG) is defined and an adaptation of the model checking algorithm is proposed. The use of the maximality semantics based verification provides new class of properties related to simultaneous progress of actions at different states.

scholarly journals A Formal Approach for RT-DVS Algorithms Evaluation Based on Statistical Model Checking

2015 ◽  
Vol 2015 ◽  
pp. 1-12 ◽  
Author(s):  
Shengxin Dai ◽  
Mei Hong ◽  
Bing Guo ◽  
Yang He ◽  
Qiongyu Zhang ◽  
...  
Keyword(s):  
Model Checking ◽  
Statistical Model ◽  
Timed Automata ◽  
Formal Approach ◽  
Statistical Model Checking ◽  
Novel Approach ◽  
Utilization Bound ◽  
Statistical Queries ◽  
Save Energy ◽  
Time Systems

Energy saving is a crucial concern in embedded real time systems. Many RT-DVS algorithms have been proposed to save energy while preserving deadline guarantees. This paper presents a novel approach to evaluate RT-DVS algorithms using statistical model checking. A scalable framework is proposed for RT-DVS algorithms evaluation, in which the relevant components are modeled as stochastic timed automata, and the evaluation metrics including utilization bound, energy efficiency, battery awareness, and temperature awareness are expressed as statistical queries. Evaluation of these metrics is performed by verifying the corresponding queries using UPPAAL-SMC and analyzing the statistical information provided by the tool. We demonstrate the applicability of our framework via a case study of five classical RT-DVS algorithms.

scholarly journals Diagnostic Model Checking for Real-Time Systems

1996 ◽  
Vol 3 (57) ◽  
Author(s):  
Kim G. Larsen ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Automatic Verification ◽  
Diagnostic Feature ◽  
Diagnostic Model ◽  
Graphical Interface ◽  
Real Time Systems ◽  
Control Protocol ◽  
Time Systems

Uppaal is a new tool suit for automatic verification of networks of<br />timed automata. In this paper we describe the diagnostic model-checking feature<br />of Uppaal and illustrates its usefulness through the debugging of (a version<br />of) the Philips Audio-Control Protocol. Together with a graphical interface of<br />Uppaal this diagnostic feature allows for a number of errors to be more easily<br />detected and corrected.

scholarly journals Compositional and Symbolic Model-Checking of Real-Time Systems

1996 ◽  
Vol 3 (59) ◽  
Author(s):  
Kim G. Larsen ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Symbolic Model Checking ◽  
Automatic Verification ◽  
Parallel Composition ◽  
Real Time Systems ◽  
Symbolic Model ◽  
Verification Tools ◽  
State Region ◽  
Time Systems

Efficient automatic model-checking algorithms for<br />real-time systems have been obtained in recent years<br />based on the state-region graph technique of Alur,<br />Courcoubetis and Dill. However, these algorithms are<br />faced with two potential types of explosion arising from<br />parallel composition: explosion in the space of control<br />nodes, and explosion in the region space over clock variables.<br />In this paper we attack these explosion problems by<br />developing and combining compositional and symbolic<br />model-checking techniques. The presented techniques<br />provide the foundation for a new automatic verification<br />tool Uppaal. Experimental results indicate that<br />Uppaal performs time- and space-wise favorably compared<br />with other real-time verification tools.

Using Timed Automata for Modeling the Clocks of Distributed Embedded Systems

2010 ◽  
pp. 172-193 ◽  
Author(s):  
Guillermo Rodriguez-Navas ◽  
Julian Proenza ◽  
Hans Hansson ◽  
Paul Pettersson
Keyword(s):  
Model Checking ◽  
Embedded Systems ◽  
Embedded System ◽  
Timed Automata ◽  
Model Checker ◽  
Distributed Embedded Systems ◽  
Temporal Behaviour ◽  
System Designer ◽  
Functional Aspects ◽  
Time Systems

Model checking is a widely used technique for the formal verification of computer systems. However, the suitability of model checking strongly depends on the capacity of the system designer to specify a model that captures the real behaviour of the system under verification. For the case of real-time systems, this means being able to realistically specify not only the functional aspects, but also the temporal behaviour of the system. This chapter is dedicated to modeling clocks in distributed embedded systems using the timed automata formalism. The different types of computer clocks that may be used in a distributed embedded system and their effects on the temporal behaviour of the system are introduced, together with a systematic presentation of how the behaviour of each kind of clock can be modeled. The modeling is particularized for the UPPAAL model checker, although it can be easily adapted to other model checkers based on the theory of timed automata.

Compositional model-checking for real-time systems

1998 ◽  
Vol 23 (1) ◽  
pp. 99
Author(s):  
Hou Jianmin ◽  
Li Xuandong ◽  
Fan Xiaocon ◽  
Zheng Guoliang
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Real Time Systems ◽  
Compositional Model ◽  
Time Systems
Sign in / Sign up

Export Citation Format

Share Document