The Power of Proofs: New Algorithms for Timed Automata Model Checking

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.

Download Full-text

Proving properties of autonomous car manoeuvres in urban traffic

it - Information Technology ◽

10.1515/itit-2021-0007 ◽

2021 ◽

Vol 0 (0) ◽

Author(s):

Maike Schwammberger

Keyword(s):

Model Checking ◽

Functional Properties ◽

Timed Automata ◽

Urban Traffic ◽

Abstract Model ◽

Automated Driving ◽

Spatial Logic

Abstract As automated driving techniques are increasingly capturing the market, it is particularly important to consider vital functional properties of these systems. We present an overview of an approach that uses an abstract model to logically reason about properties of autonomous manoeuvres at intersections in urban traffic. The approach introduces automotive-controlling timed automata crossing controllers that use the traffic logic UMLSL (Urban Multi-lane Spatial Logic) to reason about traffic situations. Safety in the context of collision freedom is mathematically proven. Liveness (something good finally happens) and fairness (no queue-jumping) are examined and verified using a model-checking tool for timed automata, UPPAAL.

Download Full-text

Timed-Automata Based Model-Checking of a Multi-Agent System: A Case Study

Journal of Software Engineering and Applications ◽

10.4236/jsea.2015.82006 ◽

2015 ◽

Vol 08 (02) ◽

pp. 43-50 ◽

Cited By ~ 1

Author(s):

Nadeem Akhtar ◽

Muhammad Nauman

Keyword(s):

Model Checking ◽

Timed Automata ◽

Multi Agent System ◽

Agent System ◽

System A ◽

Multi Agent

Download Full-text

Verified Model Checking of Timed Automata

Tools and Algorithms for the Construction and Analysis of Systems - Lecture Notes in Computer Science ◽

10.1007/978-3-319-89960-2_4 ◽

2018 ◽

pp. 61-78 ◽

Cited By ~ 13

Author(s):

Simon Wimmer ◽

Peter Lammich

Keyword(s):

Model Checking ◽

Timed Automata

Download Full-text

Model Checking via Reachability Testing for Timed Automata

BRICS Report Series ◽

10.7146/brics.v4i29.18955 ◽

1997 ◽

Vol 4 (29) ◽

Cited By ~ 3

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.

Download Full-text