From Dynamic State Machines to Promela

Authors	Massimo Benerecetti, Ugo Gentile, Stefano Marrone, Roberto Nardone, Adriano Peron, Luigi Libero Lucio Starace, and Valeria Vittorini.
conference	SPIN 2019 - 26th International SPIN Symposium on Model Checking of Software.
DOI	10.1007/978-3-030-30923-7_4

Abstract

Dynamic State Machines (DSTM) is an extension of Hierarchical State Machines recently introduced to answer some concerns raised by model-based validation of railway control systems. However, DSTM can be used to model a wide class of systems for design, verification and validation purposes. Its main characteristics are the dynamic instantiation of parametric machines and the definition of complex data types. In addition, DSTM allows for recursion and preemptive termination. In this paper we present a translation of DSTM models in Promela that can enable automatic test case generation via model checking and, at least in principle, system verification. We illustrate the main steps of the translation process and the obtained Promela encoding.

Additional notes

An implementation of the transformation chain described in this paper is available here.