Property Extraction Engine for LSCs
Authors
Jensen, Mads ; Gøttler, Rene ; Jacobsen, Michael ; Rye-Andersen, Jens Gorm
Term
4. term
Education
Publication year
2004
Abstract
Denne afhandling undersøger brugen af Live Sequence Charts (LSC'er) som et visuelt sprog til at beskrive krav til det formelle verifikationsværktøj Uppaal, som supplement til det allerede anvendte trælogiske sprog TCTL. Vi beskriver Uppaal-modeller formelt for at finde de LSC-elementer, der er relevante for verifikation. Denne LSC-undermængde specificeres formelt og implementeres i en prototype af en verifikationsmotor kaldet PEEL. Vi gennemfører eksperimenter for at vurdere LSC'er som kravspecifikationssprog for Uppaal og for at demonstrere PEEL. Resultaterne viser, at LSC'er er en intuitiv måde at specificere interobjekt-kommunikation på i Uppaal-krav, og at PEEL understøtter den valgte LSC-undermængde.
This thesis investigates using Live Sequence Charts (LSCs) as a visual language to express requirements for the formal verification tool Uppaal, alongside the tree logic language TCTL already in use. We formally describe Uppaal models to identify which LSC constructs are relevant for verifying them. We formally specify this subset of LSCs and implement it in a prototype verification engine called PEEL. We conduct experiments to evaluate LSCs as a requirements language for Uppaal and to demonstrate the PEEL prototype. The results show that LSCs provide an intuitive way to specify inter-object communication for Uppaal requirements, and that PEEL supports the selected LSC subset.
[This abstract was generated with the help of AI]
Documents