Using DEv-PROMELA for Modelling and Verification of Software

Abstract

Efficient modelling and verification of models need an accurate representation of systems. Especially, PROMELA cannot represent time as quantitative properties. That means some properties depending on time cannot be checked with SPIN model-checker. Discrete-Time approaches and dense representation of time were successfully introduced in SPIN as extensions but suffer of the expected statespace explosion problem. Another approach using discrete-event representation of time and simulation has been proposed to minimize this statespace explosion problem. In this paper, we show how this extension, DEv-PROMELA, can be used in order to model and verify software designs by combining simulation and formal verification.