Formal Extension of Use Cases for Context-Aware Verification

International audienceContext-aware veri cations are e ective techniques for au- tomating software veri cations considering speci c environ- mental conditions. Unfortunately, few existing approaches provide support for this crucial task and mainly rely on sig- ni cant e ort and expertise of the engineer. We previously proposed a DSL (called CDL) to facilitate the formaliza- tion of requirements and contexts. Experiences has shown that the number of CDL models required to precisely for- malize contexts grow rapidly according to the complexity of the system and manually writing CDL models is di cult and error prone task. In this paper, we propose a tool-supported framework that assists engineers in describing system con- texts using eXtended Use Cases (XUC). XUC models con- sistently link use cases with scenarios with respect to the domain speci cation vocabulary of the model to be checked. An industrial case study is presented to illustrate the ef- fectiveness of XUCs to generate correct and complete CDL models for formal model analysis