Issue No.10 - October (2004 vol.30)
Pao-Ann Hsiung , IEEE
Win-Bin See , IEEE
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2004.68
The growing complexity of embedded real-time software requirements calls for the design of reusable software components, the synthesis and generation of software code, and the automatic guarantee of nonfunctional properties such as performance, time constraints, reliability, and security. Available application frameworks targeted at the automatic design of embedded real-time software are poor in integrating functional and nonfunctional requirements. To bridge this gap, we reveal the design flow and the internal architecture of a newly proposed framework called Verifiable Embedded Real-Time Application Framework (VERTAF), which integrates software component-based reuse, formal synthesis, and formal verification. A formal UML-based embedded real-time object model is proposed for component reuse. Formal synthesis employs quasi-static and quasi-dynamic scheduling with automatic generation of multilayer portable efficient code. Formal verification integrates a model checker kernel from SGM, by adapting it for embedded software. The proposed architecture for VERTAF is component-based and allows plug-and-play for the scheduler and the verifier. Using VERTAF to develop application examples significantly reduced design effort and illustrated how high-level reuse of software components combined with automatic synthesis and verification can increase design productivity.
Application framework, code generation, embedded real-time software, formal synthesis, formal verification, scheduling, software components, UML modeling.
Shang-Wei Lin, Chih-Hao Tseng, Trong-Yen Lee, Pao-Ann Hsiung, Win-Bin See, "VERTAF: An Application Framework for the Design and Verification of Embedded Real-Time Software", IEEE Transactions on Software Engineering, vol.30, no. 10, pp. 656-674, October 2004, doi:10.1109/TSE.2004.68