Resource-Parameterized Timing Analysis of Real-Time Systems

Cyber-Physical Systems (CPS) are subject to platform-given resource constraints upon such resources as CPU, memory, and bus, in executing their functionalities. This causes the behavior of a verified application to deviate from its intended timing behavior when the application is integrated on a specic platform. For the same reason, a configuration of platforms cannot be independent from applications in most cases. This paper proposes a new analysis framework of real-time systems where an application and a platform can be analyzed in a fully independent way such that not only the application but also the platform once verfiied can be exploited by various applications. The dependent behaviors of application and platform are also analyzed by exploiting their individual models transformed from their independent models. To the end, we provide a highly configurable platform model that can be parameterized by various resource congurations. For analysis of application and platform models, we use two model checking techniques: symbolic and statistical model checking techniques of Uppaal. Our framework is demonstrated by a case study where a turn indicator system is analyzed with respect to various platform resource constraints.