Use Cases for Context Aware Model-Checking

Despite technical improvements in current verification tools, the increasing size of developed systems makes the detection of design defects more difficult. Context-aware Model-Checking is an effective technique for automating software verifications considering specific environmental conditions. Unfortunately, few existing approaches provide support for this crucial task and mainly rely on significant effort and expertise of the engineer. We previously proposed a DSL (called CDL) to facilitate the formalization of requirements and contexts. Experiences has shown that manually writing CDL models is difficult and error prone task. In this paper, we propose a tool-supported framework to automatically generate CDL models using eXtended Use Cases (XUC). XUC models consistently link use cases with scenarios with respect to the domain specification vocabulary of the model to be checked. We also propose a requirements specification language to fill the gap between textual requirements and CDL properties. An industrial case study is presented to illustrate the effectiveness of XUCs to generate correct and complete CDL models for formal model analysis.