Ge, Ning. Property driven verification framework: application to real time property for UML MARTE software design. PhD, Institut National Polytechnique de Toulouse, 2014
|
(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