Tick Tock Automata: A Modelling Formalism for Real World Industrial Systems
Author
Gitz-Johansen, Asger
Term
4. term
Education
Publication year
2020
Submitted on
2020-06-08
Pages
15
Abstract
Mange softwareintensive industrisystemer er sikkerhedskritiske, hvor selv små fejl kan føre til katastrofale situationer. Derfor giver modeltjek (model checking) og andre verifikationsmetoder stor værdi, fordi de kan opdage problemer, før de opstår i drift. Vi præsenterer en virkelighedsnær reaktionsorienteret semantik (reactionary semantics) i form af en automata-baseret teori, som vi kalder Tick Tock Automata. Automata er matematiske modeller med tilstande og overgange, der beskriver, hvordan et system kan udvikle sig. Teorien understøtter verifikationsteknikker som opnåelighedsanalyse (reachability analysis), der undersøger, om bestemte tilstande kan nås. Arbejdet bygger på en konkret anvendelsescase i samarbejde med lastbilproducenten HMK Bilcon A/S, hvor der er udviklet et domænespecifikt modelsprog til at understøtte en modelbaseret udviklingspipeline (MBD).
Many software-intensive industrial systems are safety-critical, where even small errors can lead to catastrophic outcomes. As a result, model checking and other verification methods are valuable because they can reveal problems before deployment. We present a real-world inspired reactionary semantics in the form of an automata-based theory called Tick Tock Automata. Automata are mathematical models with states and transitions that capture how a system can evolve. The theory supports verification techniques such as reachability analysis, which checks whether certain states can be reached. The work is grounded in a concrete use case in collaboration with the truck production company HMK Bilcon A/S, where a domain-specific modeling language was developed to support a Model-Based Development (MBD) pipeline.
[This abstract was generated with the help of AI]
Keywords
Documents