Formal Domain Engineering: From Specification to Validation
| Autor: | Mashkoor, Atif |
|---|---|
| Přispěvatelé: | Mashkoor, Atif, Development of specifications (DEDALE), Laboratoire Lorrain de Recherche en Informatique et ses Applications (LORIA), Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria)-Centre National de la Recherche Scientifique (CNRS)-Institut National Polytechnique de Lorraine (INPL)-Université Nancy 2-Université Henri Poincaré - Nancy 1 (UHP)-Institut National de Recherche en Informatique et en Automatique (Inria), Université Nancy II, Prof. Jeanine Souquières(Jeanine.Souquieres@loria.fr), ANR TACOS, CRISTAL, Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS)-Institut National de Recherche en Informatique et en Automatique (Inria)-Université Henri Poincaré - Nancy 1 (UHP)-Université Nancy 2-Institut National Polytechnique de Lorraine (INPL)-Centre National de la Recherche Scientifique (CNRS) |
| Jazyk: | angličtina |
| Rok vydání: | 2011 |
| Předmět: |
Ingénierie de domaine
Méthodes formelles B événementiel Ingénierie des besoins Domain engineering Formal methods Testing de logiciel [INFO.INFO-SE] Computer Science [cs]/Software Engineering [cs.SE] Requirements engineering Event-B Brama [INFO.INFO-SE]Computer Science [cs]/Software Engineering [cs.SE] Software testing |
| Zdroj: | Software Engineering [cs.SE]. Université Nancy II, 2011. English Software Engineering [cs.SE]. Université Nancy II, 2011. English. ⟨NNT : ⟩ |
| Popis: | The main theme of this research is to study and develop techniques for modeling of software-controlled safety-critical systems. The area we focus in this thesis is the specification of a domain, where such systems are supposed to operate, and its validation. The contribution of this thesis is twofold: First, we model the land transport domain, a good candidate for this study because of its safety-critical nature, in the formal framework of Event-B and propose some guidelines for it. Second, we present an approach, based on the technique of animation and low-cost transformations, for stepwise validation of formal specifications. Le thème principal de cette recherche est d'étudier et développer des techniques pour la modélisation des systèmes où la sécurité est critique. Cette thèse est focalisé sur l'étape de la spécification du domaine où de tels systèmes vont fonctionner, et de sa validation. La contribution de cette thèse est double. D'abord, nous modélisons le domaine des transports terrestres, un bon candidat pour cette étude en raison de sa nature critique vis-à-vis de la sécurité, dans le cadre formel de B événementiel et proposent quelques directives pour cette activité. Ensuite, nous présentons une approche, basée sur les techniques de l'animation et des transformations, pour la validation par étapes des spécifications formelles. |
| Databáze: | OpenAIRE |
| Externí odkaz: |
|