'Building Graphical Promela Models using UPPAAL GUI'
Author
Lingegowda, Vasu Hossaholal
Term
10. Term
Education
Publication year
2006
Abstract
Rapporten foreslår g-Promela, en grafisk måde at bygge modeller til SPIN-modeltjekkeren (software der systematisk kontrollerer systemadfærd). g-Promela repræsenterer centrale PROMELA-funktioner med tilstands- og overgangsdiagrammer (mærkede transitionssystemer), hvor etiketterne er gyldige PROMELA-udsagn. For at lette arbejdet skitserer vi Graphical Promela Interface (GPI), et værktøjssæt bygget oven på den eksisterende UPPAAL-GUI. Diagrammerne oversættes automatisk til tekstuel PROMELA, og SPIN verificerer temporale egenskaber (adfærd over tid) i baggrunden. En parser, som er del af et adapterværktøj mellem brugergrænsefladen og SPIN-motoren, udfører oversættelsen. Som hovedeksempel modelleres og verificeres Petersons algoritme for gensidig udelukkelse.
This report proposes g-Promela, a graphical way to build models for the SPIN model checker (software that exhaustively checks system behavior). g-Promela represents core PROMELA features with state-and-transition diagrams (labeled transition systems), where the labels are valid PROMELA statements. To make authoring easier, we sketch the Graphical Promela Interface (GPI), a toolset built on the existing UPPAAL GUI. The diagrams are automatically translated into textual PROMELA, and SPIN verifies temporal properties (behavior over time) in the background. A parser, included in an adapter between the user interface and the SPIN engine, performs the translation. As a prime example, Peterson’s Mutual Exclusion Algorithm is modeled and verified.
[This abstract was generated with the help of AI]
Documents