Multi-view modeling for MPSoC design aspects

The paper proposes a modeling approach for a MPSoC design using multi-view contracts enabling the formal interference analysis of design aspects. As an example, we focus on the behavioral, reliability and security views of the system design. For high level verification the key properties of MPSoC routing mechanism are explicitly specified and the implementation details abstracted away. The case study on an open-source MPSoC platform demonstrates that the view contracts represented as Uppaal Timed Automata can be specified and verified separately from each other provided they are non-interfering. This allows conjoining the view contracts for complete design contract without breaking the correctness of individual view contracts and avoid extensive verification of whole system design at once.