Name
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 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. |
Year | DOI | Venue |
|---|---|---|
2013 | 10.1002/cpe.2802 | Concurrency and Computation: Practice & Experience |
Keywords | DocType | Volume |
system level design,complex system,chip,formal verification,formal specification,software specification,logic design,system on chip,model checking | Journal | 25 |
Issue | ISSN | ISBN |
2 | 1532-0626 | 978-1-4244-7068-6 |
Citations | PageRank | References |
4 | 0.43 | 21 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Daniel Knorreck | 1 | 33 | 2.72 |
| Ludovic Apvrille | 2 | 136 | 22.23 |
| Renaud Pacalet | 3 | 260 | 24.51 |