Welcome!
To use the personalized features of this site, please log in or register.
If you have forgotten your username or password, we can help.
|
 |
Formal Methods Meet Domain Specific Languages
| Book Series | Lecture Notes in Computer Science |
| Publisher | Springer Berlin / Heidelberg |
| ISSN | 0302-9743 (Print) 1611-3349 (Online) |
| Volume | Volume 3771/2005 |
| Book | Integrated Formal Methods |
| DOI | 10.1007/11589976 |
| Copyright | 2005 |
| ISBN | 978-3-540-30492-0 |
| Category | Session: Applications of B |
| DOI | 10.1007/11589976_12 |
| Pages | 187-206 |
| Subject Collection | Computer Science |
| SpringerLink Date | Thursday, October 27, 2005 |
| |
|
Session: Applications of B
Formal Methods Meet Domain Specific Languages
Jean-Paul Bodeveix1  , Mamoun Filali1 , Julia Lawall2 and Gilles Muller3
| (1) |
IRIT Université Paul Sabatier, 118 route de Narbonne, F-31062 Toulouse Cedex, France |
| (2) |
DIKU University of Copenhagen, 2100 Copenhagen, Denmark |
| (3) |
Ecole des Mines de Nantes INRIA, LINA, 44307 Nantes cedex 3, France |
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.
Keywords: DSL, scheduling, formal methods, refinements, decision procedure.
Fulltext Preview (Small, Large)
|
|
|
|
|
|