Publication Type
Conference Proceeding Article
Version
publishedVersion
Publication Date
11-2012
Abstract
With the demand for new and complicated features, embedded systems are becoming more and more difficult to design and verify. Even if the design of a system is verified, how to guarantee the consistency between the design and its implementation remains a big issue. As a solution, we propose a framework that can help a system designer to model his or her embedded system using a high-level modeling language, verify the design of the system, and automatically generate executable software codes whose behavior semantics are consistent with that of the high-level model. We use two case studies to demonstrate the effectiveness of our framework.
Keywords
State Machine, Model Check, Operational Semantic, Active Object, Label Transition System
Discipline
Programming Languages and Compilers | Software Engineering
Research Areas
Software and Cyber-Physical Systems
Publication
Proceedings of the 14th International Conference on Formal Engineering Methods, , ICFEM 2012, Kyoto, Japan, November 12-16
First Page
214
Last Page
229
ISBN
9783642342806
Identifier
10.1007/978-3-642-34281-3_17
Publisher
Springer Link
City or Country
Japan
Citation
LIN, Shang-Wei; LIU, Yang; HSIUNG, Pao-Ann; SUN, Jun; and DONG, Jin Song.
Automatic generation of provably correct embedded systems. (2012). Proceedings of the 14th International Conference on Formal Engineering Methods, , ICFEM 2012, Kyoto, Japan, November 12-16. 214-229.
Available at: https://ink.library.smu.edu.sg/sis_research/5021
Creative Commons License
This work is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 4.0 International License.
Additional URL
https://doi.org/10.1007/978-3-642-34281-3_17