Automatic generation of provably correct embedded systems

Automatic generation of provably correct embedded systems

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 framew...

Full description

Saved in:
Bibliographic Details
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
Tags: Add Tag
No Tags, Be the first to tag this record!
Institution: Singapore Management University
Language: English
Description
Summary: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.

Similar Items