Modeling and Verification of Extended Timed-Arc Petri Nets
Authors
Jacobsen, Morten ; Jacobsen, Lasse ; Møller, Mikael H.
Term
4. term
Education
Publication year
2010
Abstract
Indlejret software skal ofte reagere inden for præcise tidsgrænser, og derfor bruges tidsbevidste matematiske modeller til at designe og kontrollere sådanne systemer. To udbredte familier er tidsautomater og tidsudvidede Petri-net. Forskere oversætter ofte mellem disse modeller for at genbruge analyseværktøjer og sammenligne resultater, ideelt så oversættelsen bevarer systemets adfærd eller den logik, som kravene udtrykkes i. Denne afhandling fokuserer på formel verifikation—automatisk kontrol af om en model opfylder ønskede egenskaber—af Timed-Arc Petri Nets (TAPN). I TAPN beskrives et system med pladser og overgange; flyttende markører (tokens) bærer en alder (et reelt tal), og buer er mærket med tidsintervaller, der kun tillader tokens i visse aldre at udløse en overgang. Vi udvider den grundlæggende TAPN med overførelsesbuer, inhibitorbuer og invarianter (tidsgrænser på pladser) og viser, at brug af invarianter alene gør de klassiske dækbarheds- og begrænsethedsproblemer ubesluttelige i almindelighed. Vi udtrykker egenskaber i Timed Computation Tree Logic (TCTL), en forgrenende temporallogik til at formulere “altid”, “før eller siden” og tidskrav. I modsætning til meget tidligere arbejde behandler vi TCTL’s fulde semantik, inklusive endelige maksimale forløb, som kan opstå ved deadlocks og ved både strenge og ikke-strenge invarianter. Vi identificerer en klasse af oversættelser, der bevarer TCTL, og præsenterer et generelt framework, formuleret over timede transitionssystemer, til at bevise at en oversættelse er korrekt i forhold til TCTL. Hovedideen er en én-til-mange-korrespondance: ét skridt i kildemodellen kan simuleres af flere skridt i målmodellen; når en sådan relation mellem tilstande findes, garanterer den bevarelse af fuld TCTL (eller kun sikkerhedsfragmentet, afhængigt af betingelserne). Vores framework er uafhængigt af den valgte modelleringsformalisme og matcher niveauet i moderne værktøjer som UPPAAL (www.uppaal.com), hvilket gør det direkte nyttigt for værktøjsudviklere. Vi viser eksempler fra litteraturen, der passer ind i vores framework, og peger på oversættelser, der ikke gør. For at demonstrere anvendeligheden udvikler vi to nye oversættelser fra TAPN til netværk af tidsautomater og beviser med vores framework, at begge bevarer fuld TCTL. Disse oversættelser er motiveret af nyere arbejde i værktøjet TAPAAL, hvor en tidligere oversættelse kun håndterede liveness-egenskaber for en begrænset klasse af TAPN-modeller med netop to indgående og to udgående buer pr. overgang. Efter vores bedste viden er vores oversættelser de første effektive, der bevarer fuld TCTL for vilkårlige begrænsede TAPN-modeller, og eksperimenter indikerer, at de er effektive i praksis. Vi udvider også TAPN med heltalsvariabler, så tokens kan bære heltalsværdier, der bruges i tidsintervaller og invarianter, introducerer værdiguarder og værdiginvarianter, og skitserer hvordan vores oversættelser kan udvides til at håndtere heltal med bevaret korrekthed. Vi har implementeret oversættelserne og støtte for inhibitorbuer og heltal i en prototype af verifikationsværktøjet TAPAAL (www.tapaal.net) sammen med flere praktiske forbedringer.
Embedded software often has to react within precise time bounds, so timing-aware mathematical models are used to design and check such systems. Two widely used families are timed automata and time-extended Petri nets. Researchers frequently translate between these models to reuse analysis tools and compare results, ideally so that a translation preserves the system’s behavior or the logic used to state its requirements. This thesis focuses on formal verification—automatic checking that a model satisfies desired properties—of Timed-Arc Petri Nets (TAPN). In TAPN, a system is described with places and transitions; moving markers called tokens carry an age (a real number), and arcs are labeled with time intervals that permit only tokens of certain ages to fire a transition. We extend the basic TAPN with transport arcs, inhibitor arcs, and invariants (time limits on places), and we show that using invariants alone makes the classic coverability and boundedness questions undecidable in general. We express properties in Timed Computation Tree Logic (TCTL), a branching-time temporal logic for stating “always,” “eventually,” and timing requirements. Unlike much prior work, we treat the full semantics of TCTL, including finite maximal runs that can arise from deadlocks and from both strict and non-strict invariants. We identify a class of translations that preserve TCTL and present a general framework, formulated over timed transition systems, for proving that a translation is correct with respect to TCTL. The key idea is a one-by-many correspondence: one step in the source model may be simulated by several steps in the target model; when such a relation exists between states, it guarantees preservation of the full TCTL (or only the safety fragment, depending on the conditions). Our framework is independent of the chosen modeling formalism and matches the level used in state-of-the-art tools such as UPPAAL (www.uppaal.com), making it directly useful for tool developers. We show examples from the literature that fit our framework and note cases that do not. To demonstrate applicability, we develop two new translations from TAPN to networks of timed automata and prove, using our framework, that both preserve the full TCTL. These translations are motivated by recent work in the TAPAAL tool, where an earlier translation handled only liveness properties for a restricted class of TAPN models with exactly two incoming and two outgoing arcs per transition. To our knowledge, our translations are the first efficient ones to preserve full TCTL for arbitrary bounded TAPN models, and experiments indicate they work well in practice. We also extend TAPN with integer variables so tokens can carry integer values used in time intervals and invariants, introduce value guards and value invariants, and sketch how our translations can be lifted to handle integers while retaining correctness. We have implemented the translations and support for inhibitor arcs and integers in a prototype of the TAPAAL verification tool (www.tapaal.net), along with several practical improvements.
[This abstract was generated with the help of AI]
Documents