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