Simulation model development and analysis in UNITY. We evaluate UNITY -- a computational model, specification language and proof system defined by Chandy and Misra [5] for the development of parallel and distributed programs -- as a platform for simulation model specification and analysis. We describe a UNITY-based methodology for the construction, analysis and execution of simulation models. The methodology starts with a simulation model specification in the form of a set of coupled state transition systems. Mechanical methods for mapping the transition systems first into a set of formal assertions, permitting formal verification of the transition systems, and second into an executable program are described. The methodology provides a means to independently verify the correctness of the transition systems: one can specify properties formally that the model should obey and prove them as theorems using the formal specification. The methodology is illustrated through generation of a simulation program solving the machine interference problem using the Time Warp protocol on a distributed memory parallel architecture.

References in zbMATH (referenced in 160 articles , 2 standard articles )

Showing results 1 to 20 of 160.
Sorted by year (citations)

1 2 3 ... 6 7 8 next

  1. Demasi, Ramiro; Castro, Pablo F.; Maibaum, Thomas S.E.; Aguirre, Nazareno: Simulation relations for fault-tolerance (2017)
  2. Evrard, Hugues; Lang, Frédéric: Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous (2017)
  3. Hesselink, Wim H.: Tournaments for mutual exclusion: verification and concurrent complexity (2017)
  4. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  5. Hesselink, Wim H.: Correctness and concurrent complexity of the black-white bakery algorithm (2016)
  6. Hoang, Thai Son; Schneider, Steve; Treharne, Helen; Williams, David M.: Foundations for using linear temporal logic in Event-B refinement (2016)
  7. Filali, Mamoun; Ouederni, Meriem; Raclet, Jean-Baptiste: A normalized form for FIFO protocols traces, application to the replay of mode-based protocols (2015)
  8. Futatsugi, Kokichi: Generic proof scores for generate & check method in CafeOBJ (2015)
  9. Futatsugi, Kokichi: Generate & check method for verifying transition systems in CafeOBJ (2015)
  10. Ivanov, Ievgen; Nikitchenko, Mykola; Abraham, Uri: Event-based proof of the mutual exclusion property of Peterson’s algorithm (2015)
  11. Olderog, Ernst-Rüdiger; Swaminathan, Mani: Structural transformations for data-enriched real-time systems (2015)
  12. Tarasyuk, Anton; Troubitsyna, Elena; Laibinis, Linas: Integrating stochastic reasoning into Event-B development (2015)
  13. Ogata, Kazuhiro; Futatsugi, Kokichi: Theorem proving based on proof scores for rewrite theory specifications of otss (2014)
  14. Zhao, Yongxin; Dong, Jinsong; Liu, Yang; Sun, Jun: Towards a combination of CafeOBJ and PAT (2014)
  15. Dong, Ruzhen; Faber, Johannes; Ke, Wei; Liu, Zhiming: rCOS: defining meanings of component-based software architectures (2013)
  16. Hesselink, Wim H.; IJbema, Mark: Starvation-free mutual exclusion with semaphores (2013)
  17. Hoang, Thai Son: Security invariants in discrete transition systems (2013)
  18. Ray, Sandip; Sumners, Rob: Specification and verification of concurrent programs through refinements (2013)
  19. Talpin, Jean-Pierre; Brandt, Jens; Gemünde, Mike; Schneider, Klaus; Shukla, Sandeep: Constructive polychronous systems (2013)
  20. Bae, Kyungmin; Meseguer, José: A rewriting-based model checker for the linear temporal logic of rewriting (2012)

1 2 3 ... 6 7 8 next