Title
Modeling and Validation of a Mixed-Criticality NoC Router Using the IF Language
Abstract
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.
Year
DOI
Venue
2017
10.1145/3139540.3139543
NoCArc@MICRO
Field
DocType
ISBN
Computer science,Mixed criticality,Formal specification,Real-time computing,Router,Shared resource,Formal verification,Embedded system
Conference
978-1-4503-5542-1
Citations 
PageRank 
References 
2
0.39
5
Authors
5
Name
Order
Citations
PageRank
Mourad Dridi171.90
Mounir Lallali2776.33
Stephane Rubini35712.08
Frank Singhoff49317.70
Jean-Philippe Diguet548667.41