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 \(^{\rm {\sc TM}}\).
Supported by the FRFC project “Centre Fédéré en Vérification” funded by the Belgian National Science Fundation (FNRS) under grant nr 2.4530.02.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Bosscher, D., Polak, I., Vaandrager, F.: Verification of an Audio Control Protocol. In: Langmaack, H., Roever, W.-P.d., Vytopil, J. (eds.) Formal Techniques in Real-Time and Fault-Tolerant Systems, Lübeck, Germany, vol. 863, pp. 170–192. Springer, Heidelberg (1994)
Cassez, F., Henzinger, T.A., Raskin, J.-F.: A comparison of control problems for timed and hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 134–148. Springer, Heidelberg (2002)
De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: From timed models to timed implementations. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 296–310. Springer, Heidelberg (2004)
De Wulf, M., Doyen, L., Raskin, J.-F.: Systematic implementation of real-time models (extended version). Technical Report 543, U.L.B (2005), http://www.ulb.ac.be/di/publications/
Doyen, L.: A systematic implementation of simple timed controllers. Technical Report 504, U.L.B (2003)
Henzinger, T.A., Ho, P.-H., Wong-Toi, H.: Hytech: The next generation. In: 16th Annual Real-Time Systems Symposium (RTSS), pp. 56–65. IEEE Computer Society Press, Los Alamitos (1995)
Ho, P.-H., Wong-Toi, H.: Automated analysis of an audio control protocol. In: Wolper, P. (ed.) CAV 1995. LNCS, vol. 939, pp. 381–394. Springer, Heidelberg (1995)
Lynch, N., Tuttle, M.: Hierarchical correctness proofs for distributed algorithms. In: 6th ACM Symp. on Principles of Distributed Computing, pp. 137–151 (1987)
Pettersson, P., Larsen, K.G.: Uppaal2k. Bulletin of the European Association for Theoretical Computer Science 70, 40–44 (2000)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2005 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
De Wulf, M., Doyen, L., Raskin, JF. (2005). Systematic Implementation of Real-Time Models . In: Fitzgerald, J., Hayes, I.J., Tarlecki, A. (eds) FM 2005: Formal Methods. FM 2005. Lecture Notes in Computer Science, vol 3582. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11526841_11
Download citation
DOI: https://doi.org/10.1007/11526841_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-27882-5
Online ISBN: 978-3-540-31714-2
eBook Packages: Computer ScienceComputer Science (R0)