'Building graphical-Promela models using UPPAAL GUI'
Studenteropgave: Speciale (inkl. HD afgangsprojekt)
- Vasu Hossaholal Lingegowda
10. semester, Master Software Systems Engineering SSE
'The report(v2) proposes a new graphical input specification language g-Promela for
SPIN model checker. Basic features of g-Promela language are defined using the
formal syntax of graphical elements and semantics as an extension of labeled
transition systems. The various kinds of labels of transitions are specified with
valid Promela statements. To build g-Promela models, we have sketched the
design of the Graphical Promela Interface(GPI) toolset, which is built upon the
existing UPPAAL GUI. The graphical models are then translated to textual
Promela to verify temporal properties using SPIN engine at the background.
The translation is automated by building a parser which is part of the adapter
tool built between the user interface GPI and SPIN engine. Verification is done
manually using SPIN on the example models translated to textual Promela model
from the g-Promela models built.'
Sprog | Engelsk |
---|---|
Udgivelsesdato | jan. 2007 |