This book introduces state-of-the-art verification techniques for real time embedded systems, based on the inverse method for parametric timed automata. First, the inverse method is introduced, and its interest for guaranteeing robustness in real time systems is shown. Then, different extensions are proposed, in particular to the probabilistic and hybrid cases. Various examples, both from the literature and from the industry, illustrate the techniques throughout the book.
2. The Inverse Method for Parametric Timed Automata
3. Behavioral Cartography of Timed Automata
4. Parameter Synthesis for Probabilistic Systems
5. Parameter Synthesis for Stopwatch and Hybrid Automata
6. Application to Robustness Analysis of Scheduling Problems
7. Conclusion and Perspectives