Complementarity between Simulation and Formal Verification - Transformation of PROMELA Models into FDDEVS Models: Application to a Case Study

Aznam Yacoub, Maamar Hamri, Claudia Frydman

2014

Abstract

Discrete Event system Specification (DEVS) is a simple comprehensive way to describe complex discrete event systems in a hierarchical way. Few years ago, Finite and Deterministic DEVS (FDDEVS) was introduced to support verification analysis of a subclass of DEVS problems, in the same way as formal methods. This paper presents guidelines to transform behavioral models used in formal methods like critical sections, especially described in PROMELA in this case, into FDDEVS models, and shows the benefits of such a transformation.

Paper Citation

in Harvard Style

Yacoub A., Hamri M. and Frydman C. (2014). Complementarity between Simulation and Formal Verification - Transformation of PROMELA Models into FDDEVS Models: Application to a Case Study . In Proceedings of the 4th International Conference on Simulation and Modeling Methodologies, Technologies and Applications - Volume 1: SIMULTECH, ISBN 978-989-758-038-3, pages 421-426. DOI: 10.5220/0005037904210426

in Bibtex Style

@conference{simultech14,
author={Aznam Yacoub and Maamar Hamri and Claudia Frydman},
title={Complementarity between Simulation and Formal Verification - Transformation of PROMELA Models into FDDEVS Models: Application to a Case Study},
booktitle={Proceedings of the 4th International Conference on Simulation and Modeling Methodologies, Technologies and Applications - Volume 1: SIMULTECH,},
year={2014},
pages={421-426},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0005037904210426},
isbn={978-989-758-038-3},
}

in EndNote Style

TY - CONF
JO - Proceedings of the 4th International Conference on Simulation and Modeling Methodologies, Technologies and Applications - Volume 1: SIMULTECH,
TI - Complementarity between Simulation and Formal Verification - Transformation of PROMELA Models into FDDEVS Models: Application to a Case Study
SN - 978-989-758-038-3
AU - Yacoub A.
AU - Hamri M.
AU - Frydman C.
PY - 2014
SP - 421
EP - 426
DO - 10.5220/0005037904210426