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

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

1 2 3 ... 6 7 8 next

  1. Bourke, Timothy; van Glabbeek, Robert J.; Höfner, Peter: Mechanizing a process algebra for network protocols (2016)
  2. Hesselink, Wim H.: Correctness and concurrent complexity of the black-white bakery algorithm (2016)
  3. Hoang, Thai Son; Schneider, Steve; Treharne, Helen; Williams, David M.: Foundations for using linear temporal logic in Event-B refinement (2016)
  4. Filali, Mamoun; Ouederni, Meriem; Raclet, Jean-Baptiste: A normalized form for FIFO protocols traces, application to the replay of mode-based protocols (2015)
  5. Ivanov, Ievgen; Nikitchenko, Mykola; Abraham, Uri: Event-based proof of the mutual exclusion property of Peterson’s algorithm (2015)
  6. Olderog, Ernst-Rüdiger; Swaminathan, Mani: Structural transformations for data-enriched real-time systems (2015)
  7. Tarasyuk, Anton; Troubitsyna, Elena; Laibinis, Linas: Integrating stochastic reasoning into Event-B development (2015)
  8. Hesselink, Wim H.; IJbema, Mark: Starvation-free mutual exclusion with semaphores (2013)
  9. Hoang, Thai Son: Security invariants in discrete transition systems (2013)
  10. Ray, Sandip; Sumners, Rob: Specification and verification of concurrent programs through refinements (2013)
  11. Talpin, Jean-Pierre; Brandt, Jens; Gemünde, Mike; Schneider, Klaus; Shukla, Sandeep: Constructive polychronous systems (2013)
  12. Bae, Kyungmin; Meseguer, José: A rewriting-based model checker for the linear temporal logic of rewriting (2012)
  13. Bonakdarpour, Borzoo; Bozga, Marius; Jaber, Mohamad; Quilbeuf, Jean; Sifakis, Joseph: A framework for automated distributed implementation of component-based models (2012)
  14. Clouser, Thomas; Nesterenko, Mikhail; Scheideler, Christian: Tiara: a self-stabilizing deterministic skip list and skip graph (2012)
  15. Jonsson, Bengt: Using refinement calculus techniques to prove linearizability (2012)
  16. Attie, Paul C.: On the refinement of liveness properties of distributed systems (2011)
  17. Bickford, Mark; Constable, Robert; Halpern, Joseph; Petride, Sabina: Knowledge-based synthesis of distributed systems using event structures (2011)
  18. Chandy, K.Mani; Go, Brian; Mitra, Sayan; Pilotto, Concetta; White, Jerome: Verification of distributed systems with local-global predicates (2011)
  19. Hesselink, Wim H.: Simulation refinement for concurrency verification (2011)
  20. Hesselink, Wim H.; Aravind, Alex A.: Queue based mutual exclusion with linearly bounded overtaking (2011)

1 2 3 ... 6 7 8 next