LOGIN TO YOUR ACCOUNT

Username
Password
Remember Me
Or use your Academic/Social account:

CREATE AN ACCOUNT

Or use your Academic/Social account:

Congratulations!

You have just completed your registration at OpenAire.

Before you can login to the site, you will need to activate your account. An e-mail will be sent to you with the proper instructions.

Important!

Please note that this site is currently undergoing Beta testing.
Any new content you create is not guaranteed to be present to the final version of the site upon release.

Thank you for your patience,
OpenAire Dev Team.

Close This Message

CREATE AN ACCOUNT

Name:
Username:
Password:
Verify Password:
E-mail:
Verify E-mail:
*All Fields Are Required.
Please Verify You Are Human:
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Languages: French
Types: Article
Subjects: Model Checking, Méthodes formelles, Analyse de contre-exemples, Analyse structurel, Commandes de vol, V&V, 000, Formel Methods, Counterexample Analysis, Structural Analysis, Flight Control System
Le système de commande de vol (CDV) est un des systèmes les plus critiques à bord d'un avion. Les fonctions logicielles de ce système sont donc soumises à un effort de vérification important. Chez Airbus, le développement des fonctions critiques suit une approche basée sur des modèles formels, à partir desquels la majeure partie du code embarqué est générée. Certaines vérifications peuvent ainsi s'effectuer dès le niveau de la modélisation formelle, et sont aujourd'hui réalisées par test des modèles dans un environnement de simulation. L'objet de cette thèse est d'étudier comment une technique formelle, le model-checking, s'insère dans ces vérifications amonts. La contribution comporte trois parties. La première partie tire le bilan des études passées d'Airbus sur l'application du Model Checking au système de CDV. Nous analysons notamment les caractéristiques des fonctions de CDV, et leur impact sur l'applicabilité de la technologie. Le deuxième partie complète la précédente par une nouvelle étude, expérimentant le Model Checking sur la fonction Ground Spoiler de l'A380. Les expérimentations ont permis de consolider notre analyse du positionnement du Model Checking dans le processus Airbus. Un des problèmes pratiques identifiés concerne l'exploitation des contre-exemples retournés par le model-checker, en phase de mise au point d'un modèle. La troisième partie propose une solution à ce problème, basée sur l'analyse structurelle des parties d'un modèle activées par le contre-exemple. Il s'agit, d'une part d'extraire l'information pertinente pour expliquer la violation de la propriété cible et, d'autre part de guider le model-checker vers l'exploration de comportements différents, activant d'autres parties du modèle. Un algorithme d'analyse structurelle est défini, et implémenté dans un prototype afin d'en démontrer le concept. The Flight Control System (FCS) is one of the most critical system in an aircraft. Software parts of this system are thus subject to massive vérification efforts. At Airbus, critical software function are implemented through a model based development process. Some verification can then be performed earlier on the formal model using simulation techniques. The aim of this PhD is to study how a formal method: model checking can be integrated into such a development process. PhD work is composed of three parts. Firstly we present insights from past studies about how to use model checking to verify FCS properties. We analyze FCS functions characteristics and their impact over model checking applicability. Secondly, we experiment a use of model checking on a case study: the A380 ground spoiler function. Results reinforce our proposition on the use of model checking in the FCS development process. One the technical problem deals with counterexample analysis during model verification. Finally, the third part propose a solution to that problem. It is based on a structural analysis of parts of the model activated by a counterexample. On the one hand, we extract relevant information to explain the violation of the property and, on the other hand, we guide the model checker to explore different behavior, activating different structural parts of the model. An algorithm is defined and implemented to demonstrate the functionality.
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article