Outline for an operational semantics of PROMELA. PROMELA is a high-level specification language for modeling interactions in distributed systems, and for expressing logical correctness requirements about such interactions. The model checker SPIN accepts specifications written in this language, and it can produce automated proofs for each type of property. SPIN either proves that a property is valid in the given system, or it generates a counterexample that shows that it is not. This paper contains the outline for an operational- semantics definition of PROMELA.

References in zbMATH (referenced in 28 articles )

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

1 2 next

  1. Park, Heejong; Malik, Avinash; Salcic, Zoran: Compiling and verifying SC-SystemJ programs for safety-critical reactive systems (2015)
  2. Tan, Li; Zeng, Bolong: Testing with Büchi automata: transition coverage metrics, performance analysis, and property refinement (2015)
  3. Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
  4. De Nicola, Rocco; Lluch Lafuente, Alberto; Loreti, Michele; Morichetta, Andrea; Pugliese, Rosario; Senni, Valerio; Tiezzi, Francesco: Programming and verifying component ensembles (2014)
  5. Fernández Venero, Mirtha Lina; Soares Corr^ea da Silva, Flávio: On the use of SPIN for studying the behavior of nested Petri nets (2013)
  6. Gheorghe, Marian; Ipate, Florentin; Lefticaru, Raluca; Pérez-Jiménez, Mario J.; Ţurcanu, Adrian; Cabrera, Luis Valencia; García-Quismondo, Manuel; Mierlă, Laurenţiu: 3-Col problem modelling using simple kernel P systems (2013)
  7. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  8. Leuschel, Michael; Llorens, Marisa; Oliver, Javier; Silva, Josep; Tamarit, Salvador: Static slicing of explicitly synchronized languages (2012)
  9. Ribeiro, Leila; Dos Santos, Osmar Marchi; Dotti, Fernando Luís; Foss, Luciana: Correct transformation: from object-based graph grammars to PROMELA (2012)
  10. Ipate, Florentin; Lefticaru, Raluca; Tudose, Cristina: Formal verification of P systems using Spin (2011)
  11. Donaldson, Alastair F.; Gay, Simon J.: Type inference and strong static type checking for Promela (2010)
  12. Kwiatkowska, Marta; Norman, Gethin; Parker, David: A framework for verification of software with time and probabilities (2010)
  13. Leuschel, Michael; Massart, Thierry: Efficient approximate verification of B and Z models via symmetry markers (2010)
  14. Weber, Michael: An embeddable virtual machine for state space generation (2010) ioport
  15. Ben-Ari, Mordechai: Principles of the SPIN model checker. Foreword by Gerard J. Holzmann (2008)
  16. Donaldson, Alastair F.; Miller, Alice: Automatic symmetry detection for Promela (2008)
  17. Lüdtke Ferreira, Ana Paula; Foss, Luciana; Ribeiro, Leila: Formal verification of object-oriented graph grammars specifications (2007)
  18. Song, Hosung; Compton, Kevin J.; Rounds, William C.: SPHIN: a model checker for reconfigurable hybrid systems based on SPIN (2006)
  19. Chen, J.; Cui, H.: Translation from adapted UML to Promela for CORBA-based applications (2004)
  20. del Mar Gallardo, María; Merino, Pedro; Pimentel, Ernesto: A generalized semantics of PROMELA for abstract model checking (2004)

1 2 next