Home // ICSEA 2011, The Sixth International Conference on Software Engineering Advances // View article

A Practical Method for the Reachability Analysis of Real-Time Systems Modelled as Timed Automata

Authors:
Abdeslam En-Nouaary
Rachida Dssouli

Keywords: Real-Time systems, Formal Methods, Timed Automata, Verification, Reachability Analysis.

Abstract:
Real-time systems (RTSs) interact with their environment under time constraints. Such constraints are so critical because any deviation from the specified deadlines might have severe consequences on both the human lives and the environment. To develop reliable RTSs, formal methods should be used along the development life cycle. Verification is one of these formal methods, which aims at ensuring that the system is correct before its deployment. This paper presents a new verification method for the reachability analysis of realtime systems modelled as timed automata (TA) [1]. The paper basically addresses two main issues: are all the transitions of the system executable? Are all the locations reachable from the initial location of the system? In order to answer these questions, our method uses a metric that gives the minimum delay between any state and all the transitions leaving that state.

Pages: 287 to 292

Copyright: Copyright (c) IARIA, 2011

Publication date: October 23, 2011

Published in: conference

ISSN: 2308-4235

ISBN: 978-1-61208-165-6

Location: Barcelona, Spain

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