Formal system-level design space exploration

摘要

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 communication 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 performance properties. A smart card system serves as case study to illustrate the formal verification capabilities of DIPLODOCUS.