L’objectif du project FerroCOTS est de faire évoluer l’architecture de contrôle-commande ferroviaire embarqué des relais électriques vers des Composant-sur-Etagère (COTS) programmables, ici des cartes FPGA (Field-Programmable Gate Array en anglais). Toutefois, l'absence d’une méthode appropriée de spécification et vérification formelles est un obstacle important au développement d’une architecture de contrôle-commande à base de COTS. Dans cette thèse, nous proposons tout d'abord des techniques systématiques de raffinement des exigences brutes et qui permettent de transformer des exigences informelles en des spécifications formelles, tout en guidant et assistant le processus de raffinement et l'étape de formalisation. En l'occurrence, deux méthodes de raffinement des exigences ont été développées. Le cadre de formalisation choisi pour cette méthode de formalisation des exigences est la logique temporelle CTL*, qui est un sur-ensemble des logiques CTL (Computation Tree Logic en anglais) et LTL (Linear Time Logic en anglais). Ainsi, les exigences raffinées peuvent être formalisées à l'aide de CTL*. En outre, ces formules en CTL* offrent une base formelle pour la vérification et la validation du système. Puis, à partir des spécifications formelles exprimées sous forme de propriétés CTL*, nous présentons une méthode pour générer des scénarios de test à partir des formules CTL*. La méthode de test utilise le concept de « non-vacuité » pour générer des scénarios de test « Intelligents », qui soient capables de conduire la simulation à une réfutation d’une propriété pour que les bugs dans un système sous test peuvent être détectés. / The goal of the FerroCOTS project is to develop an architecture of embedded railway command/control systems from electrical relays towards programmable Commercial-Off-The-Shelf (COTS) components, here some high-speed Field-Programmable Gate Array (FPGA) digital devices. However, the lack of appropriate formal specification and verification means is a huge obstacle to develop a COTS based control/command architecture. In this thesis, firstly we propose systematic requirement refinement techniques to transform informal requirements into formal specifications, while guiding and assisting the refinement process and the formalization step. In this case, two requirement refinement methods have been developed. The formalization framework chosen for requirement formalization is the temporal logic CTL*, which is a superset of the logic Computation Tree Logic (CTL) and the Linear Time Logic (LTL). Thus, the refined requirements are formalized using CTL*. In addition, the obtained CTL* formulas provide a formal basis for system verification and validation. On the other hand, based on formal specifications expressed as CTL* properties, we present a method for generating test cases from CTL* formulas. The test method uses the concept of non-vacuity to generate “Intelligent” test benches that are capable of driving the simulation to a property refutation so that the bug of the system under test can be detected.
| Identifer | oai:union.ndltd.org:theses.fr/2013LIL10021 |
| Date | 21 January 2013 |
| Creators | Yang, Jing |
| Contributors | Lille 1, El-Koursi, El-Miloudi, Ghazel, Mohamed |
| Source Sets | Dépôt national des thèses électroniques françaises |
| Language | English |
| Detected Language | French |
| Type | Electronic Thesis or Dissertation, Text |
Page generated in 0.002 seconds