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.