Abstract Advancements in hardware and software technologies have made possible the design of real‐time systems and applications where stringent timing constraints are imposed on critical tasks. The design of such systems is more complex than that of temporally unrestricted systems because system correctness depends on the satisfaction of functional as well as temporal requirements. To aid users in correctly and efficiently designing systems, object‐oriented frameworks provide a useful environment for significant reuse and reduction in design effort. In contrast to other application domains, there has been relatively little work on an application framework for the design of real‐time systems. Facing the growing need for real‐time applications, we propose a novel application framework called SESAG, which consists of five components, namely Specifier, Extractor, Scheduler, Allocator, and Generator. Within SESAG, several design patterns are proposed and used for the development of real‐time applications. A new evaluation metric called relative design effort is proposed for evaluating SESAG. Experiences in using SESAG show a significant increase in design productivity through design reuse and a significant decrease in design time and effort. Two complex application examples have been developed using SESAG and evaluated using the new evaluation metric. The examples demonstrate relative design efforts of at most 18% of the design efforts required by conventional methods. Copyright © 2005 John Wiley & Sons, Ltd.

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.

Producing correct software is a major goal for application frameworks that are targeted at embedded real-time systems because incorrect software is of no use and may also cause severe system damage. It is shown how formal verification can be elegantly, seamlessly, and scalably integrated into a component-based object-oriented application framework for embedded real-time systems. Two issues in such technology integration are addressed: (1) the choice of a common system model, and (2) the integration of formal synthesis and model checking. Solutions are provided, respectively, in the form of (1) proposing a new formal object-oriented model (FOOM), and (2) the execution of model checkers within synthesis algorithms. Technically, we propose a compositional software verification framework, in which model checking is employed, with state-space reduction techniques adapted for embedded real-time software. A separate verifier component is proposed for modular integration as illustrated by its implementation in the VERTAF application framework. An example illustrates the success of our approach and the benefits gained through integrating formal verification.