scholarly journals From Timed Automata to Logic - and Back

1995 ◽  
Vol 2 (2) ◽  
Author(s):  
Francois Laroussinie ◽  
Kim G. Larsen ◽  
Carsten Weise
Keyword(s):  
Model Checking ◽  
Real Time ◽  
Timed Automata ◽  
Finite Automata ◽  
Automatic Verification ◽  
Satisfiability Problem ◽  
Timed Automaton

One of the most successful techniques for automatic verification is that<br />of model checking. For finite automata there exist since long extremely<br />efficient model-checking algorithms, and in the last few years these algorithms have been made applicable to the verification of real-time automata using the region-techniques of Alur and Dill.<br />In this paper, we continue this transfer of existing techniques from the<br />setting of finite (untimed) automata to that of timed automata. In particular, a timed logic L is put forward, which is sufficiently expressive that we for any timed automaton may construct a single characteristic L formula uniquely characterizing the automaton up to timed bisimilarity. Also, we prove decidability of the satisfiability problem for L with respect to given bounds on the number of clocks and constants of the timed automata to be constructed. None of these results have as yet been succesfully accounted for in the presence of time.

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.

Schedulability Analysis for Timed Automata With Tasks

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Jinghao Sun ◽  
Nan Guan ◽  
Rongxiao Shi ◽  
Guozhen Tan ◽  
Wang Yi
Keyword(s):  
Model Checking ◽  
State Space ◽  
Real Time ◽  
Timed Automata ◽  
Schedulability Analysis ◽  
Scheduling Theory ◽  
Real Time Scheduling ◽  
Analysis Techniques ◽  
Model Complex ◽  
Time Scheduling

Research on modeling and analysis of real-time computing systems has been done in two areas, model checking and real-time scheduling theory. In model checking, an expressive modeling formalism such as timed automata (TA) is used to model complex systems, but the analysis is typically very expensive due to state-space explosion. In real-time scheduling theory, the analysis techniques are highly efficient, but the models are often restrictive. In this paper, we aim to exploit the possibility of applying efficient analysis techniques rooted in real-time scheduling theory to analysis of real-time task systems modeled by timed automata with tasks (TAT). More specifically, we develop efficient techniques to analyze the feasibility of TAT-based task models (i.e., whether all tasks can meet their deadlines on single-processor) using demand bound functions (DBF), a widely used workload abstraction in real-time scheduling theory. Our proposed analysis method has a pseudo-polynomial time complexity if the number of clocks used to model each task is bounded by a constant, which is much lower than the exponential complexity of the traditional model-checking based analysis approach (also assuming the number of clocks is bounded by a constant). We apply dynamic programming techniques to implement the DBF-based analysis framework, and propose state space pruning techniques to accelerate the analysis process. Experimental results show that our DBF-based method can analyze a TAT system with 50 tasks within a few minutes, which significantly outperforms the state-of-the-art TAT-based schedulability analysis tool TIMES.

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.

scholarly journals Learning Nondeterministic Real-Time Automata

2021 ◽  
Vol 20 (5s) ◽  
pp. 1-26
Author(s):  
Jie An ◽  
Bohua Zhan ◽  
Naijun Zhan ◽  
Miaomiao Zhang
Keyword(s):  
Active Learning ◽  
Integrated Circuits ◽  
Real Time ◽  
Learning Algorithm ◽  
Timed Automata ◽  
Finite Automata ◽  
Special Kind ◽  
Learning Problem ◽  
Equivalence Queries

We present an active learning algorithm named NRTALearning for nondeterministic real-time automata (NRTAs). Real-time automata (RTAs) are a subclass of timed automata with only one clock which resets at each transition. First, we prove the corresponding Myhill-Nerode theorem for real-time languages. Then we show that there exists a unique minimal deterministic real-time automaton (DRTA) recognizing a given real-time language, but the same does not hold for NRTAs. We thus define a special kind of NRTAs, named residual real-time automata (RRTAs), and prove that there exists a minimal RRTA to recognize any given real-time language. This transforms the learning problem of NRTAs to the learning problem of RRTAs. After describing the learning algorithm in detail, we prove its correctness and polynomial complexity. In addition, based on the corresponding Myhill-Nerode theorem, we extend the existing active learning algorithm NL* for nondeterministic finite automata to learn RRTAs. We evaluate and compare the two algorithms on two benchmarks consisting of randomly generated NRTAs and rational regular expressions. The results show that NRTALearning generally performs fewer membership queries and more equivalence queries than the extended NL* algorithm, and the learnt NRTAs have much fewer locations than the corresponding minimal DRTAs. We also conduct a case study using a model of scheduling of final testing of integrated circuits.

scholarly journals UPPAAL in 1995

1996 ◽  
Vol 3 (60) ◽  
Author(s):  
Johan Bengtsson ◽  
Kim G. Larsen ◽  
Fredrik Larsson ◽  
Paul Pettersson ◽  
Wang Yi
Keyword(s):  
Real Time ◽  
Case Studies ◽  
Theoretical Foundation ◽  
Timed Automata ◽  
Automatic Verification ◽  
Real Time Systems ◽  
The Past ◽  
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 timed automata<br />[12, 9, 4], developed during the past two years. In this paper, we summarize<br />the main features of UPPAAL in particular its various extensions developed in 1995<br />as well as applications to various case-studies, review and provide pointers to the<br />theoretical foundation.

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.

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.

Model Checking of Multitasking Real-Time Applications Based on the Timed Automata Model Using One Clock

2010 ◽  
pp. 194-218 ◽  
Author(s):  
Libor Wasziwoski ◽  
Zdenek Hanzalek
Keyword(s):  
Operating System ◽  
Model Checking ◽  
Real Time ◽  
Execution Time ◽  
Timed Automata ◽  
Real Time Operating System ◽  
Proposed Model ◽  
Real Time Applications ◽  
Real Time Application

The aim of this chapter is to show how a multitasking real-time application running under a real-time operating system can be modeled by timed automata. The application under consideration consists of several preemptive tasks and interrupts service routines that can be synchronized by events and can share resources. A real-time operating system compliant with an OSEK/VDX standard is considered for demonstration. A model checking tool UPPAAL is used to verify time and logical properties of the proposed model. Since the complexity of the model-checking verification exponentially grows with the number of clocks used in a model, the proposed model uses only one clock for measuring execution time of all modeled tasks.

Sign in / Sign up

Export Citation Format

Share Document