Contextualization and Dependency in State-Based Modelling - Application to Event-B

Dominique Méry 1, 2 Souad Kherroubi 1
1 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
Abstract : Context-awareness is an important feature in system design. We argue that in proof systems and conceptual modelling this notion should be precisely highlighted. Since we focus on conceptual modelling, understandability and clarity are provided precedence for reasoning about proofs done. In this paper, we introduce a new definition for proof context in state-based formalisms with an application in the Event-B modelling language. Furthermore, we introduce a dependency relation between two Event-B models. The contextualization of Event-B models is based on knowledge provided from domains that we classified into constraints, hypotheses and dependencies, according to their truthfulness in proofs. The dependency mechanism between two models makes possible to structure the development of systems models, by organizing phases identified in the analyzed process. These ideas are inspired by works based on the modelling of situations in situation theory that emphasize capabilities of type theory with regard to situation modelling to represent knowledge. Our approach is illustrated on small case studies, and have been validated on a development of design patterns for voting protocols.
Type de document :
Communication dans un congrès
MEDI 2017 - International Conference on Model and Data Engineering, Oct 2017, Barcelona, Spain. Springer, 10563, pp.137--152, 2017, Lecture Notes in Computer Science. 〈http://dblp.org/rec/bib/conf/medi/KherroubiM17〉. 〈10.1007/978-3-319-66854-3_11〉
Liste complète des métadonnées

https://hal.inria.fr/hal-01631017
Contributeur : Dominique Méry <>
Soumis le : mercredi 8 novembre 2017 - 15:54:18
Dernière modification le : jeudi 9 novembre 2017 - 13:08:51

Identifiants

Collections

Citation

Dominique Méry, Souad Kherroubi. Contextualization and Dependency in State-Based Modelling - Application to Event-B. MEDI 2017 - International Conference on Model and Data Engineering, Oct 2017, Barcelona, Spain. Springer, 10563, pp.137--152, 2017, Lecture Notes in Computer Science. 〈http://dblp.org/rec/bib/conf/medi/KherroubiM17〉. 〈10.1007/978-3-319-66854-3_11〉. 〈hal-01631017〉

Partager

Métriques

Consultations de la notice

21