Compositional Analysis of Timed-arc Resource Workflows with Communication
Authors
Moesgaard, Christoffer ; Birch, Sine Viesmose
Term
4. term
Education
Publication year
2015
Submitted on
2015-06-08
Pages
60
Abstract
Vi introducerer timed-arc resource workflows (TARWFN), en model for arbejdsgange, der kan gemme information mellem kørsler og kommunikere med andre workflows. Det gør modellen egnet til langvarige og sammenkoblede processer. Vi definerer begreberne lokal soundness og stærk lokal soundness, som giver forståelige korrekthedsgarantier for dele af et workflow – både når de bruges alene og når de sættes sammen i sekvens (sekventiel komposition). Vi giver en algoritme, der kan tjekke (stærk) lokal soundness ved at oversætte problemet til en allerede kendt formalisme, hvor der findes effektive tjekkere. Dermed kan man analysere workflows og samtidig bevare en meningsfuld korrekthedsforståelse, når workflows kædes sammen. For workflows med stærk lokal soundness kan vi beregne mindste og største gennemløbstid og dermed erstatte hele workflowet med én samlet overgang med tidsgrænser som betingelser. Algoritmen er implementeret i den offentligt tilgængelige, open source modeltjekker TAPAAL. Vi demonstrerer nytteværdien på et virkeligt smarthus, hvor det fulde tilstandsrum er for stort til normal udforskning. Med TARWFN-baserede approksimationer kan vi alligevel besvare spørgsmål om huset inden for rimelig tid.
We present timed-arc resource workflows (TARWFN), a workflow model that can remember information between runs and communicate with other workflows, making it suitable for long-running and interconnected processes. We define local soundness and strong local soundness, providing clear correctness guarantees for parts of a workflow—both when used alone and when connected end-to-end (sequential composition). We provide an algorithm to check (strong) local soundness by translating the problem into a formalism that already has efficient checking algorithms. This enables practical analysis of workflows while preserving a meaningful notion of soundness under sequential composition. For strongly locally sound workflows, we can compute minimum and maximum execution times and replace the entire workflow with a single transition guarded by these time bounds. The algorithm is implemented in the publicly available, open-source model checker TAPAAL. We demonstrate its usefulness on a real smart house, where the state space is too large for standard exploration; with TARWFN-based approximations we can still conclusively answer questions about the house within reasonable time.
[This abstract was generated with the help of AI]
Keywords
Documents