Summary form only given, as follows. The complete presentation was not made available for publication as part of the conference proceedings. The Hi-Five framework is a holistic framework for the validation and verification of embedded real-time systems. The framework reuses the state of the art in formal verification and test case generation to provide an end-to-end solution to mitigate the typically high cost of validation and verification activities. The framework is based on a literate formal specification language, the Timed Abstract State Machine (TASM) language. The TASM language captures the three key aspects of embedded real-time system behavior, namely functional behavior, timing, and resource consumption. These aspects can be captured and analyzed using the TASM language and its associated toolset. Using the TASM language, the Hi-Five framework models systems at multiple levels of abstraction and provides traceability between related models. The framework provides an overarching approach to system engineering by leveraging the formal semantics of the TASM language to automate verification and test case generation. During the early phases of system engineering, incorporating nonfunctional properties in system models is an approximate activity at best. For example, before an implementation exists, it is challenging to specify behavior related to time and resource consumption. Nevertheless, gaining insight into the system designs, before the system is implemented, yields considerable benefits in terms of cost and time savings. For example, evaluating design properties, such as end-to-end latency and Quality of Service can help optimize designs or select between competing designs. The Hi-Five approach to resolving this apparent paradox is to use bi-directional traceability through levels of abstraction. The end result of the approach is an integrated development environment where the effect of changes can be efficiently managed and enforced through levels of abstraction, from requirements to implementation.

In this paper, we present some of the issues encountered when trying to apply model-driven approaches to the engineering of real-time systems. In real-time systems, quantitative values of time, as reflected through the duration of actions, are central to the system's correctness. We review basic time concepts and explain how time is handled in different modeling languages. We expose the inherent paradox of incorporating quantitative time-dependent behavior in high-level models. High-level models are typically built before the system is implemented, which makes quantitative time metrics difficult to predict since these metrics depend heavily on implementation details. We provide some possible answers to this paradox and explain how the Timed Abstract State Machine (TASM) language helps address some of these issues.