DocumentCode :
3191751
Title :
Automating Context Description for Software Formal Verification
Author :
Raji, Amine ; Dhaussy, Philippe ; Aizier, Bruno
Author_Institution :
LabSTICC, Univ. Europeenne de Bretagne, Brest, France
fYear :
2010
fDate :
3-3 Oct. 2010
Firstpage :
13
Lastpage :
18
Abstract :
Formal methods have increasingly been recognized as effective techniques for automating software verifications to satisfy quality and reliability. However, using such techniques within industrial development processes takes an important part of the development time and budget due to the complexity of developed software. Context aware techniques can circumvent this complexity by reducing the scope of the verification to some precise system configurations. Unfortunately, few existing approaches provide support for this crucial task and mainly rely on significant effort and expertise of the engineer. In this paper, we propose a tool-based framework that automate the description of the system contexts to improve the integration of formal verification techniques into industrial engineering methods. Models describing contexts are automatically generated from use cases and scenarios using model transformations. Then, requirements are checked considering generated contexts to reduce the complexity of the proof.
Keywords :
program verification; software quality; software reliability; context aware techniques; context description automation; formal methods; industrial engineering; model transformations; software complexity; software formal verification; software quality; software reliability; Automata; Context; Context modeling; Explosions; Object oriented modeling; Software; Unified modeling language; Context Description Language; Formal verifications; UML activity diagram; model transformation; property patterns; use cases;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Model-Driven Engineering, Verification, and Validation (MoDeVVa), 2010 Workshop on
Conference_Location :
Oslo
Electronic_ISBN :
978-0-7695-4384-0
Type :
conf
DOI :
10.1109/MoDeVVa.2010.13
Filename :
5772245
Link To Document :
بازگشت