Restricting DEv-PROMELA with a hierarchy of simulation formalisms

The DEv-PROMELA formalism is a new formalism that allows combining formal verification and discrete event simulation. In this paper, we propose to use a hierarchy of simulation formalisms to restrict the DEv-PROMELA language. From sequential machine to the most expressive DEv-PROMELA formalism, this hierarchy helps designers to design models and to analyze systems in a progressive manner.