Premium
Formal system‐level design space exploration
Author(s) -
Knorreck Daniel,
Apvrille Ludovic,
Pacalet Renaud
Publication year - 2013
Publication title -
concurrency and computation: practice and experience
Language(s) - English
Resource type - Book series
SCImago Journal Rank - 0.309
H-Index - 67
eISSN - 1532-0634
pISSN - 1532-0626
ISBN - 978-1-4244-7068-6
DOI - 10.1002/cpe.2802
Subject(s) - computer science , unified modeling language , programming language , formal verification , systemc , formal methods , semantics (computer science) , mathematical proof , embedded system , geometry , mathematics , software
SUMMARY 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. Copyright © 2012 John Wiley & Sons, Ltd.