Systematic implementation of real-time models

Abstract

Recently we have proposed the "almost ASAP" semantics as an alternative semantics for timed automata. This semantics is useful when modeling real-time controllers: control strategies modeled with this semantics are robust and implementable (without making the synchrony hypothesis). We show in this paper how to effectively encode this semantics using timed automata along with their classical semantics. We have implemented a tool set that allows us to verify, using HYTECH and UPPAAL, the almost ASAP behavior of controllers and generate automatically provably correct code from verified models. To illustrate the applicability of our results, we show how we have synthesized the code for the Philips Audio Control Protocol for LEGO MINDSTORMS™. © Springer-Verlag Berlin Heidelberg 2005.