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

Additional URL

https://doi.org/10.1007/978-3-642-34281-3_17

Share

COinS