Modular Timing Analysis of Component-Based Real-Time Embedded Systems
The correctness of complex real-time embedded systems not only depends on the functional behavior but also on the timing. Nowadays such systems are commonly developed according to a component-based development paradigm, where different stakeholders develop subsystems in parallel. The correctness of the real-time behavior is addressed in a cumbersome integration and configuration phase at the end of the development process, that in the worst case may fail. As a consequence, conflicts are discovered rather late in the development process, often being required to change or redesign larger parts of the system. Approaches using formal models provide techniques to support an early analysis, allowing us to detect potential conflicts of the real-time behavior much earlier in the development process. To be applicable in practice, such formal approaches need to fulfill a number of requirements. One of the most critical requirements is to be able to handle complex architectures, consisting of a huge number of components.
Further, a parallel development process needs to be supported and analysis activities need to be applicable by different stakeholders in parallel. In addition, typical activities need to be supported, as in the case of testing, allowing us to decide whether the behavior of the formal models fits the behavior of the later implementation.
In this thesis a formal framework is defined that allows us to model and analyze the real-time behavior of component-based real-time embedded systems in a modular way that scales. Modularity is achieved in such a manner that the real-time behavior is analyzed by applying only local checks using neighbored components. The correctness of the overall system can be concluded from the local checks. By doing so, the defined framework allows us to analyze systems of arbitrary size, while only being required to apply isolated local checks. Further, individual checks can be applied in parallel, supporting a distributed and parallel development process also in the case of testing.
The solution proposed in this work is applied on an existing development framework and process that is taken from the automotive domain. The approach is evaluated using a real running example and it is shown how typical activities like modeling and testing are supported.