UNITY

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 153 articles , 2 standard articles )

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

1 2 3 ... 6 7 8 next

  1. Evrard, Hugues; Lang, Frédéric: Automatic distributed code generation from formal models of asynchronous processes interacting by multiway rendezvous (2017)
  2. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  3. Hesselink, Wim H.: Correctness and concurrent complexity of the black-white bakery algorithm (2016)
  4. Hoang, Thai Son; Schneider, Steve; Treharne, Helen; Williams, David M.: Foundations for using linear temporal logic in Event-B refinement (2016)
  5. Filali, Mamoun; Ouederni, Meriem; Raclet, Jean-Baptiste: A normalized form for FIFO protocols traces, application to the replay of mode-based protocols (2015)
  6. Futatsugi, Kokichi: Generate & check method for verifying transition systems in CafeOBJ (2015)
  7. Futatsugi, Kokichi: Generic proof scores for generate & check method in CafeOBJ (2015)
  8. Ivanov, Ievgen; Nikitchenko, Mykola; Abraham, Uri: Event-based proof of the mutual exclusion property of Peterson’s algorithm (2015)
  9. Olderog, Ernst-Rüdiger; Swaminathan, Mani: Structural transformations for data-enriched real-time systems (2015)
  10. Tarasyuk, Anton; Troubitsyna, Elena; Laibinis, Linas: Integrating stochastic reasoning into Event-B development (2015)
  11. Dong, Ruzhen; Faber, Johannes; Ke, Wei; Liu, Zhiming: rCOS: defining meanings of component-based software architectures (2013)
  12. Hesselink, Wim H.; IJbema, Mark: Starvation-free mutual exclusion with semaphores (2013)
  13. Hoang, Thai Son: Security invariants in discrete transition systems (2013)
  14. Ray, Sandip; Sumners, Rob: Specification and verification of concurrent programs through refinements (2013)
  15. Talpin, Jean-Pierre; Brandt, Jens; Gemünde, Mike; Schneider, Klaus; Shukla, Sandeep: Constructive polychronous systems (2013)
  16. Bae, Kyungmin; Meseguer, José: A rewriting-based model checker for the linear temporal logic of rewriting (2012)
  17. Bonakdarpour, Borzoo; Bozga, Marius; Jaber, Mohamad; Quilbeuf, Jean; Sifakis, Joseph: A framework for automated distributed implementation of component-based models (2012)
  18. Clouser, Thomas; Nesterenko, Mikhail; Scheideler, Christian: Tiara: a self-stabilizing deterministic skip list and skip graph (2012)
  19. Jonsson, Bengt: Using refinement calculus techniques to prove linearizability (2012)
  20. Attie, Paul C.: On the refinement of liveness properties of distributed systems (2011)

1 2 3 ... 6 7 8 next