Sciweavers

Share
CL
2008
Springer

Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems

8 years 2 months ago
Automatic synthesis and verification of real-time embedded software for mobile and ubiquitous systems
Currently available application frameworks that target the automatic design of real-time embedded software are poor in integrating functional and non-functional requirements for mobile and ubiquitous systems. In this work, we present the internal architecture and design flow of a newly proposed framework called Verifiable Embedded Real-Time Application Framework (VERTAF), which integrates three techniques namely software component-based reuse, formal synthesis, and formal verification. Component reuse is based on a formal unified modeling language (UML) real-time embedded object model. Formal synthesis employs quasi-static and quasi-dynamic scheduling with multi-layer portable efficient code generation, which can output either real-time operating systems (RTOS)-specific application code or automatically generated real-time executive with application code. Formal verification integrates a model checker kernel from state graph manipulators (SGM), by adapting it for embedded software. Th...
Pao-Ann Hsiung, Shang-Wei Lin
Added 09 Dec 2010
Updated 09 Dec 2010
Type Journal
Year 2008
Where CL
Authors Pao-Ann Hsiung, Shang-Wei Lin
Comments (0)
books