sg 14(2): e4

Research Article

Formal Framework to improve the reliability of concurrent and collaborative learning games

Download296 downloads
  • @ARTICLE{10.4108/sg.1.2.e4,
        author={I. Mounier and A. Yessad and T. Carron and F. Kordon and J-M.  Labat},
        title={Formal Framework to improve the reliability of concurrent and collaborative learning games},
        journal={EAI Endorsed Transactions on Serious Games},
        volume={1},
        number={2},
        publisher={ICST},
        journal_a={SG},
        year={2014},
        month={5},
        keywords={Concurrent and Collaborative learning Game; Scenario Modeling; Scenario Verification; Model Checking; Symmetric Petri Nets},
        doi={10.4108/sg.1.2.e4}
    }
    
  • I. Mounier
    A. Yessad
    T. Carron
    F. Kordon
    J-M. Labat
    Year: 2014
    Formal Framework to improve the reliability of concurrent and collaborative learning games
    SG
    ICST
    DOI: 10.4108/sg.1.2.e4
I. Mounier1,2, A. Yessad1,2, T. Carron1,2,3, F. Kordon1,2, J-M. Labat1,2
  • 1: Sorbonne Universités, UPMC Univ Paris 06, UMR 7606, LIP6, 75005, Paris, France
  • 2: CNRS, UMR 7606, LIP6
  • 3: Université de Savoie, 73000, Chambéry, France

Abstract

Multi-player learning games are complex software applications resulting from a costly and complex engineering process, and involving multiple stakeholders (domain experts, teachers, game designers, programmers, testers, etc.). Moreover, they are dynamic systems that evolve over time and implement complex interactions between objects and players. Usually, once a learning game is developed, testing activities are conducted by humans who explore the possible executions of the game’s scenario to detect bugs. The complexity and the dynamic nature of multiplayer learning games enforces the complexity of testing activities. Indeed, it is impracticable to explore manually all possible executions due to their huge number. Moreover, the test cannot verify some properties on multi-player and collaborative scenarios, such as paths leading to deadlock between learners or prevent learners to meet all objectives and win the game. This type of properties should be verified at the design stage. We propose a framework enabling a formal modeling of game scenarios and an associated automatic verification of learning game’s scenario at the design stage of the development process.We use Symmetric Petri nets as a modeling language and choose to verify properties by means of model checkers. This paper discusses the possibilities offered by this framework to verify learning game’s properties before the programming stage.