Skip to Main content Skip to Navigation
Journal articles

DEv-PROMELA: modeling, verification, and validation of a video game by combining model-checking and simulation

Abstract : Modeling, verifying, and validating are essential steps in order to build systems and software that do what designers expect. If formal verification, and especially model-checking, is a popular method for proving the correctness of properties, its efficiency depends on the accuracy of the used models and the quality of abstractions. As a consequence, applying verification techniques on large-scale complex software like video games is hard without strong assumptions and simplifications. Simulation models are generally more accurate than verification models, but it is often harder to verify them. Combined formalisms that take the benefits of both model-checking and discrete-event simulation represent a good deal between both of these families, although strong engineering expertise remains necessary to define the relevant tests and scenarios. This paper proposes an approach to build this kind of formalism through the example of DEv-PROMELA, which is built by combining Discrete-event System Specification formalism and PROMELA language. Then, it shows how combined formalisms can be used for modeling, verifying, and validating complex software like video games by using both formal-based and simulation-based verification and validation.
Complete list of metadata

https://hal-amu.archives-ouvertes.fr/hal-03538522
Contributor : MAAMAR EL AMINE HAMRI Connect in order to contact the contributor
Submitted on : Friday, January 21, 2022 - 10:04:05 AM
Last modification on : Wednesday, March 2, 2022 - 3:31:28 PM

Identifiers

Collections

Citation

Aznam Yacoub, Maamar El Amine Hamri, Claudia Frydman. DEv-PROMELA: modeling, verification, and validation of a video game by combining model-checking and simulation. SIMULATION-TRANSACTIONS OF THE SOCIETY FOR MODELING AND SIMULATION INTERNATIONAL, 2020, 96 (11), ⟨10.1177/0037549720946107⟩. ⟨hal-03538522⟩

Share

Metrics

Record views

19