Abstract
In this paper, we relate an experiment whose aim is to study how to combine two existing approaches for ensuring software correctness: Domain Specific Languages (DSLs) and formal methods. As examples, we consider the Bossa DSL and the B formal method. Bossa is dedicated to the development of process schedulers and has been used in the context of Linux and Chorus. B is a refinement based formal method which has especially been used in the domain of railway systems. In this paper, we use B to express the correctness of a Bossa specification. Furthermore, we show how B can be used as an alternative to the existing Bossa tools for the production of certified schedulers.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Abrial, J.-R.: The B-Book: Assigning programs to meanings. Cambridge University Press, Cambridge (1996)
Badeau, F., Amelot, A.: Using B as a high level programming language in an industrial project: Roissy VAL. In: Treharne, H. King, S., Henson, M., Schneider, S., (eds.). ZB 2005: Formal Specification and Development in Z and B. LNCS, vol. 2215, Guildford, UK, pp. 298–315. Springer, Heidelberg (2005)
Basu, A., Hayden, M., Morrisett, G., von Eicken, T.: A language-based approach to protocol construction. In: Proceedings of the ACM SIGPLAN Workshop on Domain Specific Languages, Paris, France (January 1997)
Behm, P., Desforges, P., Meynadier, J.-M.: Météor: An industrial success in formal development. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, p. 26. Springer, Heidelberg (1998)
Cottet, F., Delacroix, J., Kaiser, C., Mammeri, Z.: Scheduling in Real-Time Systems. Wiley, West Sussex (2002)
Henriksen, J., Jensen, J., Jorgensen, M., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Workshop on Tools and Algorithms for the Construction and Analysis of Systems, Aarhus, May 1995, pp. 58–73 (1995), http://www.brics.dk/~mona
Jaluna. Jaluna Osware, http://www.jaluna.com
Kumar, S., Mandelbaum, Y., Yu, X., Li, K.: ESP: a language for programmable devices. In: Proceedings of the ACM SIGPLAN 2001 conference on Programming Language Design and Implementation, Snowbird, UT, June 2001, pp. 309–320 (2001)
Lawall, J., Le Meur, A.-F., Muller, G.: On designing a target-independent DSL for safe OS process-scheduling components. In: Karsai, G., Visser, E. (eds.) GPCE 2004. LNCS, vol. 3286, pp. 436–455. Springer, Heidelberg (2004)
Leijen, D., Meijer, E.: Domain specific embedded compilers. In: Proceedings of the Second Conference on Domain-Specific Languages (DSL 1999), Austin, TX, October 1999, pp. 109–122 (1999)
Thomas, W.: Automata on infinite objects. In: Leeuwen, J.v. (ed.) Handbook of Theoretical Computer Science, pp. 133–192. MIT Press, Cambridge (1990)
van Deursen, A., Klint, P., Visser, J.: Domain-specific languages: An annotated bibliography. ACM SIGPLAN Notices 35(6), 26–36 (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
Bodeveix, JP., Filali, M., Lawall, J., Muller, G. (2005). Formal Methods Meet Domain Specific Languages. In: Romijn, J., Smith, G., van de Pol, J. (eds) Integrated Formal Methods. IFM 2005. Lecture Notes in Computer Science, vol 3771. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11589976_12
Download citation
DOI: https://doi.org/10.1007/11589976_12
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-30492-0
Online ISBN: 978-3-540-32240-5
eBook Packages: Computer ScienceComputer Science (R0)