Modeling and Verification of Real Time Systems

3,5 ECTS

Aim: The aim of this lecture is to provide to students the theory of automata and some of their applications. In the first part, we introduce the basic theory of finite automata and its application to indexing structures and pattern matching. In the second part, we show how quantitative information can be added to finite automata, we present timed automata an extension of finite automata used for checking real time properties of distributed systems.


Content:

  1. Finite Automata and Indexing Structures
    • Words, regular languages and automata
    • Operations on languages and automata : set operations, product, star
    • Determinization, Minimization
    • Quotient of automata
    • Borders, Periods
    • Suffix automaton, Suffix tree
    • Compaction, Minimization of a cyclic automata
    • Forbidden minimal words
  2. Timed Automata and Model Checking
    • Modeling using timed automata
    • Clock Regions
    • Clock Zones
    • Difference Bound Matrices
    • UPPALL Model Checker
    • Timed game automata