Home // VALID 2011, The Third International Conference on Advances in System Testing and Validation Lifecycle // View article

A Zone-based Reachability Analysis of Variable Driven Timed Automata

Authors:
Omer Nguena-Timo
Antoine Rollet

Keywords: reachability analysis, zone, timed systems, data-flow, urgent edges.

Abstract:
In this paper, we propose an algorithm for efficient reachability analysis of Variable Driven Timed Automata (VDTA). VDTA is a new timed behavioural model for data-flow reactive systems in which inputs and outputs are modelled by variables. Such an approach is commonly used in the industry. Reachability analysis is often the basis of model-checking, test generation (especially Test Purpose approach), or control algorithms. For example, a model-based testing framework with VDTA derives test cases by performing a region-based reachability analysis. Thus, an efficient analysis is needed. We propose an algorithm based on the zone abstraction. The algorithm not only checks the reachability, but it also computes timed sequences of input updates required to reach a target. In practice, it is more efficient than region based one.

Pages: 51 to 57

Copyright: Copyright (c) IARIA, 2011

Publication date: October 23, 2011

Published in: conference

ISSN: 2308-4316

ISBN: 978-1-61208-168-7

Location: Barcelona, Spain

Dates: from October 23, 2011 to October 29, 2011