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.

From Dynamic State Machines to Promela / Benerecetti, Massimo; Gentile, Ugo; Nardone, Roberto; Peron, Adriano; Starace, LUIGI LIBERO LUCIO; Vittorini, Valeria; Marrone, Stefano. - 11636:(2019), pp. 56-73. [10.1007/978-3-030-30923-7_4]

From Dynamic State Machines to Promela

Massimo Benerecetti
;
Ugo Gentile;Roberto Nardone;Adriano Peron;Luigi Libero Lucio Starace;Valeria Vittorini;
2019

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.
2019
978-3-030-30923-7
From Dynamic State Machines to Promela / Benerecetti, Massimo; Gentile, Ugo; Nardone, Roberto; Peron, Adriano; Starace, LUIGI LIBERO LUCIO; Vittorini, Valeria; Marrone, Stefano. - 11636:(2019), pp. 56-73. [10.1007/978-3-030-30923-7_4]
File in questo prodotto:
Non ci sono file associati a questo prodotto.

I documenti in IRIS sono protetti da copyright e tutti i diritti sono riservati, salvo diversa indicazione.

Utilizza questo identificativo per citare o creare un link a questo documento: https://hdl.handle.net/11588/775734
Citazioni
  • ???jsp.display-item.citation.pmc??? ND
  • Scopus 1
  • ???jsp.display-item.citation.isi??? 0
social impact