When developing complex solutions consisting of multiple components developed and delivered by different stakeholders, the integration of these components becomes a crucial step. While component based frameworks exist supporting an upfront agreement on syntactical aspects using interfaces, other aspects such as timing or resource consumption are addressed rather late during integration. This leads often to several problems as missed deadlines, discovered late in the overall development process. This problems require changes of design decisions made in early stages. Changing design decisions in a late development stage often requires to reimplement a substantial part of already implemented functionalities. To avoid this effect, in the context of this research area a framework is developed to support an upfront verification of the timing behavior at the level of components. The approach is evaluated using the AUTOSAR framework. The timing behavior of AUTOSAR components is represented using the well known model of timed automata. How such a timed automaton can look like and how model checking capabilities can be applied is shown in our publications. Furthermore, we show an approach for automatically transform a given AUTOSAR architecture to a set of timed automata. A reasoning-scheme supporting a scalable model-checking of derived timed automata models is also introduced.
References
You find our publications for this research area at the official project website.