Formal Methods Meet Domain Specific Languages
Résumé
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.
Domaines
Langage de programmation [cs.PL]
Fichier principal
Formal Methods Meet Domain Specific Languages.pdf (273.07 Ko)
Télécharger le fichier
Origine : Fichiers éditeurs autorisés sur une archive ouverte