Integrating Domain-Based Features into Event-B: a Nose Gear Velocity Case Study

Abstract : This paper presents the formal modelling of a nose gear velocity system, a software-based system for estimating the ground velocity of an aircraft. We employ the Event-B modelling language to conduct this case study. Event-B allows us to construct and verify the formal model of the system using the incremental refinement-based process. The main goal of the case study is to highlight the need for separating and integrating explicit semantics of application domain into the formal development process. Traditionally in Event-B development, domain descriptions of systems containing domain knowledge are treated as second-class citizens, and the modelling is implicit and usually distributed between the requirements model and the system model. In this paper, we highlight the need for explicit modelling of domain contexts as first-class citizens, and we illustrate concepts related to implicit and explicit semantics with the help of an example in Event-B.
Type de document :
Communication dans un congrès
Ladjel Bellatreche; Yannis Manolopoulos. Model and Data Engineering - 5th International Conference, MEDI 2015, Sep 2015, Rhodes, Greece. springer, lncs 9344, pp.89-102, 2015, Model and Data Engineering - 5th International Conference, MEDI 2015. 〈http://link.springer.com/book/10.1007%2F978-3-319-23781-7〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01245991
Contributeur : Dominique Méry <>
Soumis le : jeudi 17 décembre 2015 - 20:50:48
Dernière modification le : mercredi 22 novembre 2017 - 11:02:25

Identifiants

  • HAL Id : hal-01245991, version 1

Collections

Citation

Dominique Méry, Sawant Rushikesh, Anton Tarasyuk. Integrating Domain-Based Features into Event-B: a Nose Gear Velocity Case Study. Ladjel Bellatreche; Yannis Manolopoulos. Model and Data Engineering - 5th International Conference, MEDI 2015, Sep 2015, Rhodes, Greece. springer, lncs 9344, pp.89-102, 2015, Model and Data Engineering - 5th International Conference, MEDI 2015. 〈http://link.springer.com/book/10.1007%2F978-3-319-23781-7〉. 〈hal-01245991〉

Partager

Métriques

Consultations de la notice

371