OATAO - Open Archive Toulouse Archive Ouverte Open Access Week

Property driven verification framework: application to real time property for UML MARTE software design

Ge, Ning. Property driven verification framework: application to real time property for UML MARTE software design. PhD, Institut National Polytechnique de Toulouse, 2014

[img]
Preview
(Document in English)

PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
3MB

Official URL: http://ethesis.inp-toulouse.fr/archive/00002711/

Abstract

Automatic formal verification such as model checking faces the combinatorial explosion issue. This limits its application in indus- trial projects. This issue is caused by the explosion of the number of states during system’s execution , as it may easily exceed the amount of available computing or storage resources. This thesis designs and experiments a set of methods for the development of scalable verification based on the property-driven approach. We propose efficient approaches based on model checking to verify real-time requirements expressed in large scale UML-MARTE real-time system designs. We rely on the UML and its profile MARTE as the end-user modeling language, and on the Time Petri Net (TPN) as the verification language. The main contribution of this thesis is the design and implementation of a property-driven verification prototype toolset dedicated to real-time properties verification for UML-MARTE real-time software designs. We validate this toolset using an avionic use case and its user requirements. The whole prototype toolset includes five contributions: definition of real-time property specific execution semantics for UML-MARTE architecture and behavior models; specification of real- time requirements relying on a set of verification dedicated atomic real- time property patterns; real-time property specific observer-based model checking approach in TPN; real-time property specific state space reduction approach for TPN; and fault localization approach in model checking.

Item Type:PhD Thesis
Uncontrolled Keywords:
Institution:Université de Toulouse > Institut National Polytechnique de Toulouse - Toulouse INP (FRANCE)
Laboratory name:
Research Director:
Marc, Pantel and Aît Ameur, Yamine
Statistics:download
Deposited On:05 Sep 2014 21:58

Repository Staff Only: item control page