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

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

1 2 next

  1. Brunner, Julian; Lammich, Peter: Formal verification of an executable LTL model checker with partial order reduction (2018)
  2. Jantsch, Simon; Norrish, Michael: Verifying the LTL to Büchi automata translation via very weak alternating automata (2018)
  3. Park, Heejong; Malik, Avinash; Salcic, Zoran: Compiling and verifying SC-SystemJ programs for safety-critical reactive systems (2015)
  4. Tan, Li; Zeng, Bolong: Testing with Büchi automata: transition coverage metrics, performance analysis, and property refinement (2015)
  5. Vu, Dieu-Huong; Chiba, Yuki; Yatake, Kenro; Aoki, Toshiaki: Checking the conformance of a Promela design to its formal specification in Event-B (2015)
  6. De Nicola, Rocco; Lluch Lafuente, Alberto; Loreti, Michele; Morichetta, Andrea; Pugliese, Rosario; Senni, Valerio; Tiezzi, Francesco: Programming and verifying component ensembles (2014)
  7. Fernández Venero, Mirtha Lina; Soares Corrêa da Silva, Flávio: On the use of SPIN for studying the behavior of nested Petri nets (2013)
  8. 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)
  9. Perna, Juan I.; George, Chris: Model checking RAISE applicative specifications (2013)
  10. Leuschel, Michael; Llorens, Marisa; Oliver, Javier; Silva, Josep; Tamarit, Salvador: Static slicing of explicitly synchronized languages (2012)
  11. Ribeiro, Leila; Dos Santos, Osmar Marchi; Dotti, Fernando Luís; Foss, Luciana: Correct transformation: from object-based graph grammars to PROMELA (2012)
  12. Ipate, Florentin; Lefticaru, Raluca; Tudose, Cristina: Formal verification of P systems using Spin (2011)
  13. Donaldson, Alastair F.; Gay, Simon J.: Type inference and strong static type checking for Promela (2010)
  14. Kwiatkowska, Marta; Norman, Gethin; Parker, David: A framework for verification of software with time and probabilities (2010)
  15. Leuschel, Michael; Massart, Thierry: Efficient approximate verification of B and Z models via symmetry markers (2010)
  16. Weber, Michael: An embeddable virtual machine for state space generation (2010) ioport
  17. Ben-Ari, Mordechai: Principles of the SPIN model checker. Foreword by Gerard J. Holzmann (2008)
  18. Donaldson, Alastair F.; Miller, Alice: Automatic symmetry detection for Promela (2008)
  19. Lüdtke Ferreira, Ana Paula; Foss, Luciana; Ribeiro, Leila: Formal verification of object-oriented graph grammars specifications (2007)
  20. Song, Hosung; Compton, Kevin J.; Rounds, William C.: SPHIN: a model checker for reconfigurable hybrid systems based on SPIN (2006)

1 2 next