'Building graphical-Promela models using UPPAAL GUI'
Author
Lingegowda, Vasu Hossaholal
Term
10. Term
Education
Publication year
2007
Abstract
Denne rapport introducerer g-Promela, et nyt grafisk input-sprog til SPIN, et værktøj der tjekker, om modeller af systems adfærd opfylder bestemte egenskaber over tid. I stedet for kun at skrive modeller som tekst kan brugeren opbygge dem som diagrammer, der derefter oversættes til Promela, det tekstbaserede sprog som SPIN bruger. Vi definerer g-Promelas grafiske syntaks og betydning ved at udvide mærkede transitionssystemer – forstået som tilstande forbundet af pile (overgange), hvor hver overgang er forsynet med gyldige Promela-udsagn, der beskriver systemets handlinger eller betingelser. For at bygge g-Promela-modeller skitserer vi Graphical Promela Interface (GPI), baseret på den eksisterende UPPAAL-brugerflade. De grafiske modeller oversættes automatisk til tekstuel Promela via en parser i et adapterværktøj, som forbinder GPI med SPIN-motoren. Efter oversættelsen kan tidslige egenskaber (adfærd over tid) verificeres med SPIN. Rapporten demonstrerer processen ved manuelt at verificere eksempelmodeller, der er oversat fra g-Promela til Promela.
This report introduces g-Promela, a new graphical input language for SPIN, a tool that checks whether system models satisfy certain properties over time. Instead of writing models only as text, users can build them as diagrams and then translate them into Promela, the textual language used by SPIN. We define the graphical syntax and meaning by extending labeled transition systems—think of states connected by arrows (transitions), where each transition is labeled with valid Promela statements that describe actions or conditions. To create g-Promela models, we sketch the Graphical Promela Interface (GPI), built on the existing UPPAAL graphical interface. The graphical models are automatically translated into textual Promela by a parser within an adapter that links the GPI user interface to the SPIN engine. After translation, temporal properties (behavior over time) can be verified using SPIN. The report demonstrates this workflow by manually verifying example models translated from g-Promela to Promela.
[This abstract was generated with the help of AI]
Documents