Michael Hofbaur, Franz Wotawa
Modern artifacts are typically composed of many system components and exhibit a complex pattern of continuous/discrete behaviors. A concurrent hybrid automaton is a powerful modeling concept to capture such a system's behavior in terms a concurrent composition of hybrid automata for the individual system components. Because of the potentially large number of modes of the concurrent automaton model it is non-trivial to validate the composition such that every possible operational mode leads to a causally valid dynamic model for the overall system. This paper presents a novel model analysis method that validates the automata composition without the necessity to analyze a prohibitively large number of modes. We achieve this by formulating the exhaustive causal analysis of hybrid automata as a diagnosis problem. This provides causal specifications of the component automata and enables us to efficiently calculate the causal relationships for their concurrent composition and thus validate a concurrent automaton model.
Subjects: 9.1 Causality; 1.5 Diagnosis