A new application framework called Verifiable Embedded Real-Time Application
Framework (VERTAF) is proposed for embedded real-time application
development, with the aim of reducing design errors and increasing design
productivity. VERTAF is an integration of three technologies: object-oriented,
software component, and formal verification. It consists of five software
components: Implanter, Modeler, Scheduler, Verifier,
and Generator. Experiences of using VERTAF show a significant increase
in design productivity through design reuse, and a significant decrease in
design time and effort through design verification.