Formal Methods Meet Domain Specific Languages | Zendy

Jean-Paul Bodeveix | Zendy; Mamoun Filali | Zendy; Julia Lawall | Zendy; Gilles Muller | Zendy

AI Assistant Blog Pricing

Home ZAIA Blog

Open Access

Formal Methods Meet Domain Specific Languages

Author(s) -

Jean-Paul Bodeveix,

Mamoun Filali,

Julia Lawall,

Gilles Muller

Publication year - 2005

Publication title -

lecture notes in computer science

Language(s) - English

Resource type - Book series

SCImago Journal Rank - 0.249

H-Index - 400

eISSN - 1611-3349

pISSN - 0302-9743

ISBN - 3-540-30492-4

DOI - 10.1007/11589976_12

Subject(s) - correctness , computer science , programming language , formal methods , digital subscriber line , b method , domain specific language , domain (mathematical analysis) , context (archaeology) , process (computing) , software engineering , theoretical computer science , mathematics , telecommunications , mathematical analysis , paleontology , biology

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.

The content you want is available to Zendy users.

Already have an account? Click here to sign in.

Having issues? You can contact us here

Accelerating Research