Use Cases for Context Aware Model-Checking

  • Amine Raji
  • Philippe Dhaussy
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7167)


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.


Model Transformation Sequence Diagram Activity Diagram Requirement Document Domain Element 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Dhaussy, P., Pillain, P.-Y., Creff, S., Raji, A., Le Traon, Y., Baudry, B.: Evaluating Context Descriptions and Property Definition Patterns for Software Formal Validation. In: Schürr, A., Selic, B. (eds.) MODELS 2009. LNCS, vol. 5795, pp. 438–452. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  2. 2.
    Dhaussy, P., Boniol, F., De Belloy, S.E., Auvray, J., Landel, E.: Using context descriptions and property definition pattern for software formal verification. Modevva (2008)Google Scholar
  3. 3.
    Dhaussy, P., Creff, S., Plllain, P., Leilde, V.: CDL: a context description language, synthax and semantics, ENSTA-Bretagne, Tech. Rep. (2010)Google Scholar
  4. 4.
    Dwyer, M.B., Avrunin, G.S., Corbett, J.C.: Patterns in Property Specifications for Finite-State Verification. In: International Conference on Software Engineering, pp. 411–420 (1999)Google Scholar
  5. 5.
    OMG, UML 2.1.2 Superstructure, pp. 1–738 (2007)Google Scholar
  6. 6.
    Wang, Z., Elbaum, S., Rosenblum, D.: Automated generation of context-aware tests. In: 29th International Conference on Software Engineering, ICSE 2007, pp. 406–415 (2007)Google Scholar
  7. 7.
    Ben Mokhtar, S., Fournier, D., Georgantas, N., Issarny, V.: Context-Aware Service Composition in Pervasive Computing Environments. In: Guelfi, N., Savidis, A. (eds.) RISE 2005. LNCS, vol. 3943, pp. 129–144. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  8. 8.
    Stevens, P.: On Use Cases and Their Relationships in the Unified Modelling Language. In: Hussmann, H. (ed.) FASE 2001. LNCS, vol. 2029, pp. 140–155. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  9. 9.
    Gutiérrez, J.J., Nebut, C., Escalona, M.J., Mejías, M., Ramos, I.M.: Visualization of Use Cases through Automatically Generated Activity Diagrams. In: Czarnecki, K., Ober, I., Bruel, J.-M., Uhl, A., Völter, M. (eds.) MODELS 2008. LNCS, vol. 5301, pp. 83–96. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  10. 10.
    Zhu, H., Jin, L.: Automating scenario-driven structured requirements engineering. In: The 24th Annual International Computer Software and Applications Conference, COMPSAC 2000, pp. 311–316 (2002)Google Scholar
  11. 11.
    Zhu, H., Jin, L., Diaper, D., Bai, G.: Software requirements validation via task analysis. Journal of Systems and Software 61(2), 145–169 (2002)CrossRefGoogle Scholar
  12. 12.
    Berthomieu, B., Ribet, P.O., Vernadat, F.: The tool TINA - Construction of abstract state spaces for Petri Nets and Time Petri Nets. International Journal of Production Research 42(14), 298–304 (2004)Google Scholar
  13. 13.
    Berthomieu, B., Bodeveix, J., Filali, M.: The syntax and semantics of Fiacre, Tech. Rep. (2007)Google Scholar
  14. 14.
    Almendros-Jiménez, J.M., Iribarne, L.: Describing Use Cases with Activity Charts. In: Wiil, U.K. (ed.) MIS 2004. LNCS, vol. 3511, pp. 141–159. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  15. 15.
    Bastide, R.: An Integration of Task and Use-Case Meta-models. In: Jacko, J.A. (ed.) HCII 2009, Part I. LNCS, vol. 5610, pp. 579–586. Springer, Heidelberg (2009)CrossRefGoogle Scholar
  16. 16.
    Mustafiz, S., Sun, X., Kienzle, J., Vangheluwe, H.: Model-Driven Assessment of Use Cases for Dependable Systems. In: Wang, J., Whittle, J., Harel, D., Reggio, G. (eds.) MODELS 2006. LNCS, vol. 4199, pp. 558–573. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  17. 17.
    Alrajeh, D., Kramer, J., Russo, A., Uchitel, S.: Learning operational requirements from goal models. In: Proceedings of the 2009 IEEE 31st International Conference on Software Engineering, pp. 265–275 (2009)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Amine Raji
    • 1
  • Philippe Dhaussy
    • 1
  1. 1.LISyC – ENSTA-BretagneUniversité Européenne de BretagneBrest Cedex 9France

Personalised recommendations