Un cadre formel pour l'intégration de connaissances du domaine dans la conception des systèmes : application au formalisme Event-B

Souad Kherroubi 1
1 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : This thesis aims at defining techniques to better exploit the knowledge provided from the domain in order to account for the reality of systems described as complex and critical. Modeling is an essential step in performing verifications and expressing properties that a system must satisfy according to the needs and requirements established in the specifications. Modeling is a representation that simplifies the reality of a system. However, a complex system can not be reduced to a model. A model that represents a system must always fit into its observational theory to account for any anomalies that it may contain. Our study clearly shows that the context is the first issue to deal with as the main source of conflict in the design process of a system. The approach adopted in this thesis is that of integrating knowledge of the domain by associating the system to design with declarative formalisms qualified of descriptive ones that we call ontologies. We pay a particular attention to the Event-B formalism, whose correct-by-construction approach called refinement is the main mechanism at the heart of this formalism, which makes it possible to make proofs on abstract representations of systems for expressing and verifying properties of safety and invariance. The first problem treated is the representation and modeling of contextual knowledge in V&V of models. Following to the study looked at the different sources of conflict, we established new definitions and rules for a refinement context knowledge extraction for Event-B V&V. A study of logical formalisms that represent and interpret the context allowed us to define a new mechanism for better structuring Event-B models. A second study concerns the contribution that domain knowledge can make to the V&V of models. We define a logic for the Event-B formalism with domain constraints based on the description logic, and we define rules to integrate domain knowledge for model V&V. The evaluation of the proposals made deal with very complex case studies such as voting systems whose design patterns are also developed in this thesis. We raise fundamental issues about the complementarity that the integration of domain knowledge can bring to Event-B models by refinement using ontological reasoning, and we propose to define a new structures for a partially automated extraction on both levels, namely the V&V
Complete list of metadatas

Cited literature [248 references]  Display  Hide  Download

https://hal.univ-lorraine.fr/tel-02094875
Contributor : Thèses Ul <>
Submitted on : Wednesday, April 10, 2019 - 9:33:03 AM
Last modification on : Thursday, April 11, 2019 - 1:18:54 AM

File

DDOC_T_2018_0230_KHERROUBI.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : tel-02094875, version 1

Citation

Souad Kherroubi. Un cadre formel pour l'intégration de connaissances du domaine dans la conception des systèmes : application au formalisme Event-B. Théorie et langage formel [cs.FL]. Université de Lorraine, 2018. Français. ⟨NNT : 2018LORR0230⟩. ⟨tel-02094875⟩

Share

Metrics

Record views

73

Files downloads

101