Skip to Main content Skip to Navigation
Journal articles

Formal system-level design space exploration

Abstract : DIPLODOCUS is a UML profile intended for the modeling and the formal verification of real-time and embedded applications commonly executed on complex Systems-on-Chip. DIPLODOCUS implements the Y-chart approach, that is, application and HW architecture (e.g., CPUs, bus, memories) are first described independently and are subsequently related to each other in a mapping stage. Abstract tasks and commu- nication primitives are therefore mapped onto platform elements like buses and CPUs. DIPLODOCUS endows all models with a formal semantics, thereby paving the way for formal proofs both before and after mapping. More concretely, application, architecture, and mapping models can be edited in TTool – an open-source toolkit – using UML diagrams. Then, pre-mapping or post-mapping UML models may be automatically transformed into a LOTOS-based representation. This specification is in turn amenable to model-checking techniques to evaluate properties of the system, for example, safety, schedulability, and per- formance properties. A smart card system serves as case study to illustrate the formal verification capabilities of DIPLODOCUS.
Complete list of metadata
Contributor : Renaud Pacalet Connect in order to contact the contributor
Submitted on : Wednesday, July 8, 2020 - 8:42:51 AM
Last modification on : Saturday, April 9, 2022 - 11:02:01 AM

Links full text



Daniel Knorreck, Ludovic Apvrille, Renaud Pacalet. Formal system-level design space exploration. Concurrency and Computation: Practice and Experience, Wiley, 2012, 25 (2), pp.250-264. ⟨10.1002/cpe.2802⟩. ⟨hal-02893082⟩



Record views