‌FORMATS is celebrating its 20th anniversary in 2022. To commemorate  this, we will be holding a special session at the conference, featuring presentations from some of the founding members of the community:

Patricia Bouyer‬ (CNRS, LMF): Zone-based verification of timed automata: Extrapolations, simulations and what next?

Abstract:

Timed automata have been introduced by Rajeev Alur and David Dill in the early 90’s. In the last decades, timed automata have become the de facto  model for the verification of real-time systems. Algorithms for timed  automata are based on the traversal of their state-space using zones as  a symbolic representation. Since the state-space is infinite, termination relies on finite abstractions that yield a finite representation of the reachable states. The first solution to get finite abstractions was based on extrapolations of zones, and has been implemented in the industry-strength tool Uppaal. A different approach based on simulations between zones has emerged in the last ten years, and has been implemented in the fully open source tool TChecker. The 
simulation-based approach has led to new efficient algorithms for reachability and liveness in timed automata, and has also been extended to richer models like weighted timed automata, and timed automata with diagonal constraints and updates. In this article, we survey the extrapolation and simulation techniques, and discuss some open challenges for the future.

 Thomas A. Henzinger (IST Austria): A Personal History of Formal Modeling and Analysis of Timed Systems before there was FORMATS

Abstract:

The 1990s were a time of much activity in developing formal models and analysis techniques for timed systems. I will give a personal view of some of the early developments in which I was involved, including freeze quantifiers and event clocks; location invariants and time divergence; symbolic region algebras and fixpoints; hybrid automata and timed games.

 Kim Guldstrand Larsen (Aalborg University): On-line Testing and Monitoring of Real-Time Systems — Revisited

Abstract:

In this talk we highlight and revisit on-line testing and monitoring of  real-time systems with respect to  properties expressed as Timed I/O Automata, Metric Interval Temporal Logic or Timed Büchi Automata. We offer efficient symbolic online algorithms in a number of settings, exploiting so-called zones well-known from efficient model checking of Timed Automata. The settings considered include treatment of non-determinism, time divergence, timing uncertainty, remote and  contextual monitoring and testing, and, on-line minimum time estimates before conclusive verdicts can be made.