VERTAF: an application framework for the design and verification of embedded real-time software
| Autor: | Chih-Hao Tseng, Win-Bin See, Trong-Yen Lee, Pao-Ann Hsiung, Shang-Wei Lin, Jin-Ming Fu |
|---|---|
| Rok vydání: | 2004 |
| Předmět: |
Model checking
Object-oriented programming Non-functional requirement Computer science business.industry Real-time computing Reuse Software portability Embedded software Software Unified Modeling Language Component-based software engineering Software construction Code generation Software verification and validation Software requirements Software architecture business Formal verification computer Software verification computer.programming_language |
| Zdroj: | IEEE Transactions on Software Engineering. 30:656-674 |
| ISSN: | 0098-5589 |
| DOI: | 10.1109/tse.2004.68 |
| Popis: | 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 quasistatic and quasidynamic 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. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|