Author(s)
Term
4. term
Education
Publication year
2020
Submitted on
2020-06-08
Pages
15 pages
Abstract
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.
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.
Keywords
Documents
Colophon: This page is part of the AAU Student Projects portal, which is run by Aalborg University. Here, you can find and download publicly available bachelor's theses and master's projects from across the university dating from 2008 onwards. Student projects from before 2008 are available in printed form at Aalborg University Library.
If you have any questions about AAU Student Projects or the research registration, dissemination and analysis at Aalborg University, please feel free to contact the VBN team. You can also find more information in the AAU Student Projects FAQs.