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:
On Thursday 28/09/2017 and Friday 29/09/2017 due to system maintenance you might experience some downtimes to claim, search and validator services that will also affect the portal. We apologize for the inconvenience.
fbtwitterlinkedinvimeoflicker grey 14rssslideshare1
Languages: French
Types: Article
Subjects: Logique Temporelle Linéaire, Analyse Dynamique, Analyse Statique, Logiciels critiques, 000, Linear Temporal Logic, Dynamic analysis, Static analysis, Critical software
La vérification de logiciels est une activité dont l'importance est cruciale pour les logiciels embarqués critiques. Les différentes approches envisageables peuvent être classées en quatre catégories : les méthodes d'analyse statique non formelles, les méthodes d'analyse statique formelles, les méthodes d'analyse dynamique non formelles et les méthodes d'analyse dynamique formelles. L'objectif de cette thèse est de vérifier des propriétés temporelles dans un cadre industriel, par analyse dynamique formelle. La contribution comporte trois parties. Un langage adapté à l'expression des propriétés à vérifier, tirées du contexte industriel d'Airbus, a été dé ni. Il repose notamment sur la logique temporelle linéaire mais également sur un langage d'expressions régulières. La vérification d'une propriété temporelle s'effectue sur une trace d'exécution d'un logiciel, générée à partir d'un cas de test pré-existant. L'analyse statique est utilisée pour générer la trace en fonction des informations nécessaires à la vérification de la propriété temporelle formalisée. Cette approche de vérification propose une solution pragmatique au problème posé par le caractère ni des traces considérées. Des adaptations et des optimisations ont également été mises en œuvre pour améliorer l'efficacité de l'approche et faciliter son utilisation dans un contexte industriel. Deux prototypes ont été implémentés, des expérimentations ont été menées sur différents logiciels d'Airbus. Software Verification is decisive for embedded software. The different verification approaches can be classified in four categories : non formal static analysis, formal static analysis, non formal dynamic analysis and formal dynamic analysis. The main goal of this thesis is to verify temporal properties on real industrial applications, with the help of formal dynamic analysis. There are three parts for this contribution. A language, which is well adapted to the properties we want to verify in the Airbus context was defined. This language is grounded on linear temporal logic and also on a regular expression language. Verification of a temporal property is done on an execution trace, generated from an existing test case. Generation also depends on required information to verify the formalized property. Static analysis is used to generate the trace depending on the formalized property. The thesis also proposes a pragmatic solution to the end of trace problem. In addition, specific adaptations and optimisations were defined to improve efficiency and user-friendliness and thus allow an industrial use of this approach. Two applications were implemented. Some experiments were led on different Airbus software.
  • No references.
  • No related research data.
  • No similar publications.

Share - Bookmark

Cite this article