Tick Tock Automata: A Modelling Formalism for Real World Industrial Systems

Student thesis: Master thesis (including HD thesis)

  • Asger Gitz-Johansen
4. term, Software, Master (Master Programme)
Many software intense industry systems are safety critical, meaning even small errors can lead to catastrophical scenarios. Such systems are ripe for reaping the benefits of model checking and verification techniques. We present a real-world inspired reactionary semantics in the form of an automata based theory that we call Tick Tock Automata, sup- porting verification techniques such as reachability analysis. The theory is based on a specific use case, in collaboration with the truck production company HMK Bilcon A/S, where a domain specific modeling language have been developed to support a Model Based Development (MBD) pipeline.
Publication date8 Jun 2020
Number of pages15
External collaboratorHMK Bilcon A/S
Mathias Bach Svendsen mbs@hmkbilcon.dk
ID: 333799324