Timed Automata: Semantics, Algorithms and Tools
5星 · 超过95%的资源 需积分: 10 105 浏览量
2010-09-29
18:34:34
上传
评论
收藏 371KB PDF 举报 
Timed Automata: Semantics, Algorithms and Tools
Johan Bengtsson and Wang Yi
Uppsala University
Email: {johanb,yi}@it.uu.se
Abstract. This chapter is to provide a tutorial and pointers to results and related
work on timed automata with a focus on semantical and algorithmic aspects of
verification tools. We present the concrete and abstract semantics of timed au-
tomata (based on transition rules, regions and zones), decision problems, and
algorithms for verification. A detailed description on DBM (Difference Bound
Matrices) is included, which is the central data structure behind several verifica-
tion tools for timed systems. As an example, we give a brief introduction to the
tool UPPAAL.
1 Introduction
Timed automata is a theory for modeling and verification of real time systems. Exam-
ples of other formalisms with the same purpose, are timed Petri Nets, timed process
algebras, and real time logics [BD91,RR88,Yi91,NS94,AH94,Cha99]. Following the
work of Alur and Dill [AD90,AD94], several model checkers have been developed with
timed automata being the core of their input languages e.g. [Yov97,LPY97]. It is fair
to say that they have been the driving force for the application and development of the
theory. The goal of this chapter is to provide a tutorial on timed automata with a focus
on the semantics and algorithms based on which these tools are developed.
In the original theory of timed automata [AD90,AD94], a timed automaton is a finite-
state Büchi automaton extended with a set of real-valued variables modeling clocks.
Constraints on the clock variables are used to restrict the behavior of an automaton, and
Büchi accepting conditions are used to enforce progress properties. A simplified ver-
sion, namely Timed Safety Automata is introduced in [HNSY94] to specify progress
properties using local invariant conditions. Due to its simplicity, Timed Safety Au-
tomata has been adopted in several verification tools for timed automata e.g. UPPAAL
[LPY97] and Kronos [Yov97]. In this presentation, we shall focus on Timed Safety Au-
tomata, and following the literature, refer them as Timed Automata or simply automata
when it is understood from the context.
The rest of the chapter is organized as follows: In the next section, we describe the syn-
tax and operational semantics of timed automata. The section also addresses decision
problems relevant to automatic verification. In the literature, the decidability and unde-
cidability of such problems are often considered to be the fundamental properties of a
computation model. Section 3 presents the abstract version of the operational semantics
based on regions and zones. Section 4 describes the data structure DBM (Difference
剩余41页未读，继续阅读
资源评论
xingyang59092013-07-07很不错的资源
