The TASM Language and the Hi-Five Framework: Specification, Validation, and Verification of Embedded Real-Time Systems
Martin Ouimet, Kristina Lundqvist · 2007
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.