Dynamic reactive modules Conference Paper


Author(s): Fisher, Jasmin; Henzinger, Thomas A; Ničković, Dejan; Piterman, Nir; Singh, Anmol V; Vardi, Moshe Y
Title: Dynamic reactive modules
Title Series: LNCS
Affiliation IST Austria
Abstract: 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 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.
Conference Title: CONCUR: Concurrency Theory
Volume: 6901
ISBN: 978-3-95977-017-0
Publisher: Schloss Dagstuhl - Leibniz-Zentrum für Informatik  
Location: Berlin, Heidelberg
Date Published: 2011-01-01
Start Page: 404
End Page: 418
Sponsor: ERC Advanced Grant QUAREM, FWF NFN Grant S11402-N23 (RiSE), EU NOE Grant ArtistDesign
URL:
DOI: 10.1007/978-3-642-23217-6_27
Open access: no
IST Austria Authors
  1. Thomas A. Henzinger
    415 Henzinger
Related IST Austria Work