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 23 articles )

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

1 2 next

  1. Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
  2. De Nicola, Rocco; Lluch Lafuente, Alberto; Loreti, Michele; Morichetta, Andrea; Pugliese, Rosario; Senni, Valerio; Tiezzi, Francesco: Programming and verifying component ensembles (2014)
  3. 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)
  4. 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)
  5. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  6. Leuschel, Michael; Llorens, Marisa; Oliver, Javier; Silva, Josep; Tamarit, Salvador: Static slicing of explicitly synchronized languages (2012)
  7. Ribeiro, Leila; Dos Santos, Osmar Marchi; Dotti, Fernando Luís; Foss, Luciana: Correct transformation: from object-based graph grammars to PROMELA (2012)
  8. Ipate, Florentin; Lefticaru, Raluca; Tudose, Cristina: Formal verification of P systems using Spin (2011)
  9. Donaldson, Alastair F.; Gay, Simon J.: Type inference and strong static type checking for Promela (2010)
  10. Kwiatkowska, Marta; Norman, Gethin; Parker, David: A framework for verification of software with time and probabilities (2010)
  11. Leuschel, Michael; Massart, Thierry: Efficient approximate verification of B and Z models via symmetry markers (2010)
  12. Weber, Michael: An embeddable virtual machine for state space generation (2010)
  13. Ben-Ari, Mordechai: Principles of the SPIN model checker. Foreword by Gerard J. Holzmann (2008)
  14. Donaldson, Alastair F.; Miller, Alice: Automatic symmetry detection for Promela (2008)
  15. Lüdtke Ferreira, Ana Paula; Foss, Luciana; Ribeiro, Leila: Formal verification of object-oriented graph grammars specifications (2007)
  16. del Mar Gallardo, María; Merino, Pedro; Pimentel, Ernesto: A generalized semantics of PROMELA for abstract model checking (2004)
  17. Leue, Stefan; Mayr, Richard; Wei, Wei: A scalable incomplete test for message buffer overflow in Promela models (2004)
  18. Pingree, Paula J.; Mikk, Erich: The HiVy tool set (2004)
  19. Baldamus, Michael; Schröder-Babo, Jochen: p2b: A translation utility for linking Promela and symbolic model checking (tool paper) (2001)
  20. Kamel, Moataz; Leue, Stefan: Formalization and validation of the general inter-ORB protocol (GIOP) using PROMELA and SPIN (2000)

1 2 next