Dynamic Reactive Modules

  • Fisher J ,
  • Henzinger T ,
  • Nickovic D ,
  • Piterman N ,
  • Singh A ,
  • Vardi M ,
  • Jasmin Fisher

22nd International Conference on Concurrency Theory, LNCS 6901, pp. 404-418 |

Published by Springer Verlag

State-transition systems communicating by shared variables have been the underlying model of choice for applications of model checking. Such formalisms, however, have difficulty with modeling process creation or death and communication reconfigurability. Here, we introduce “dynamic reactive modules”, (DRM) a state-transition modeling formalism that supports dynamic reconfiguration and creation/death of processes. The resulting formalism supports two types of variables, data variables and reference variables. Reference variables enable changing the connectivity between processes and referring to instances of processes. We show how this new formalism supports natural parallel composition and refinement through trace containment. DRM provide a natural language for modeling (and ultimately reasoning about) biological systems and multiple threads communicating through shared variables.