Automating Context Description for Software Formal Verification

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.