Modeling and Validation of a Mixed-Criticality NoC Router Using the IF Language

In Mixed-Criticality Systems (MCS), high-critical real-time and low-critical real-time applications share the same hardware platform. Today MCS must also be implementable on NoC-based architectures. Those applications exchange messages with different timing requirements through the same network. Sharing resources between flows in a NoC can lead to unpredictable latencies and subsequently complicate the implementation of MCS in many-core architectures. A solution is that NoC routers provide guarantees for high-critical communications with a minimum impact on performances for low-critical communications. We propose a new router called DAS, which exhibits such properties to support MCS applications. Moreover we introduce the first formal verification of the MCS properties of a NoC-router. We detail a formal specification of the DAS router, with the IF language, in order to verify its ability to support MCS applications. We also describe the validation approach of this specification based on those properties and using the IF toolset.