Automatic generation of provably correct embedded systems

• Main Authors: LIN, Shang-Wei, LIU, Yang, HSIUNG, Pao-Ann, SUN, Jun, DONG, Jin Song
• Format: text
• Language: English
• Published: Institutional Knowledge at Singapore Management University 2012
• Subjects: State Machine; Model Check; Operational Semantic; Active Object; Label Transition System; Programming Languages and Compilers; Software Engineering
• Online Access: https://ink.library.smu.edu.sg/sis_research/5021; https://ink.library.smu.edu.sg/context/sis_research/article/6024/viewcontent/automatic.pdf
• Institution: Singapore Management University

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.