Automatic Generation of Observers for the Dala Robot with TTG
Saddek Bensalem, Marius Dorel Bozga, Matthieu Gallien, François Félix Ingrand, Moez Krichen, Stavros Tripakis, Hichem Arioui, Rochdi Merzouki, Hadj Ahmed Abbassi · AIP conference proceedings · 2008
We report on the use of the timed test generator tool TTG as an automatic generator of observers for monitoring purposes for the Dala Robot (LAAS) case study. The starting point is a plan, which is taken to be a high‐level specification. This plan is automatically translated into a network of timed automata written in IF language. From the latter an observer is automatically synthesized. The observer checks whether a sequence of observations conforms to the specification. We applied our method on a non‐conforming trace of length 60. The non‐conformance was detected using discrete‐time semantics.