Name
Abstract | ||
|---|---|---|
Code generators play a critical role in the Model Based Development of complex software systems. This is particularly true in the automotive domain, where the code auto-generated from Simulink/Stateflow models is directly flashed onto embedded controllers. Testing based approaches are popular for validating the translation of models to code. However, these approaches cannot guarantee the absence of bugs introduced during translation. We use translation validation as an alternative to testing. By checking the equivalence between a Stateflow model and C code, it can provide formal guarantees about the absence of bugs introduced during translation. To the best of our knowledge, this is the first application of translation validation to code generation from hierarchical state-machine modeling languages. Our approach builds upon the significant progress over the last few years in software model-checking: we use a state-of-the-art off-the-shelf software model-checker, CBMC, to make translation validation practical for a complex modeling language like Stateflow. We have applied this approach to Stateflow models from the automotive domain. |
Year | DOI | Venue |
|---|---|---|
2014 | 10.1145/2593069.2593237 | Design Automation Conference |
Keywords | Field | DocType |
C language,automotive engineering,program compilers,program testing,program verification,visual languages,C code,CBMC,Simulink model,Stateflow model,autogenerated code,automotive domain,bug absence,code generators,complex modeling language,complex software systems,embedded controllers,formal guarantees,hierarchical state-machine modeling languages,model-based development,off-the-shelf software model-checker,testing-based approach,translation validation,C,State flow,Translation validation | Programming language,Computer science,Modeling language,Model-based design,Real-time computing,Software system,Code generation,Software,Equivalence (measure theory),Stateflow,Automotive industry | Conference |
ISSN | Citations | PageRank |
0738-100X | 4 | 0.40 |
References | Authors | |
14 | 3 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Prahladavaradan Sampath | 1 | 64 | 7.65 |
| A. C. Rajeev | 2 | 46 | 4.34 |
| Ramesh, S. | 3 | 4 | 0.40 |