Embedded safety-critical systems must not only be functionally correct but must also provide timely service. It is thus important to have rigorous analysis techniques for determining timing properties of such systems. We consider a layered design process, where timing analysis is conducted based on contracts. More precisely, we develop a contract theory, considering resource supplies and demands of components at each layer allowing to consider timing behavior and interferences due to shared resource usage of components. Therefore, engineers can negotiate specifications of the individual components a priori including expected availability of resources of a target platform. The developed contract theory supports independent implementability. So contracts can be independently refined and implemented, knowing that no integration issues will occur due to shared resource usage. The approach exploits omega-languages, which enables analysis techniques based on model-checking.
July / 2014
ARAMiS – Automotive, Railway and Avionic Multicore System