Modeling and Verification of Timed-Arc Petri Net
Translated title
Modellering og Verifikation af Timed-Arc Petri Net
Authors
Jacobsen, Morten ; Jacobsen, Lasse ; Møller, Mikael Harkjær
Term
2. term
Education
Publication year
2010
Pages
120
Abstract
Indlejret software skal opfylde strenge tidskrav for at være pålideligt og sikkert. Sådanne systemer modelleres ofte med tidsafhængige formalismer som timed automata og tidsudvidede Petri-net. I denne afhandling arbejder vi med Timed-Arc Petri Nets (TAPN), hvor tokens (markører) har en realværdet “alder”, og buer mellem pladser og overgange er beskyttet af tidsintervaller, der bestemmer, hvilke tokens der må udløse en overgang. Vi udvider den grundlæggende TAPN-model med transportbuer, inhibitorbuer og invarianter, og viser samtidig at invarianter alene gør problemerne dækbarhed og begrænsethed uafgørlige (dvs. der findes ingen algoritme, der kan afgøre dem i alle tilfælde). Vi fokuserer på formel verificering (modeltjekning) med Timed Computation Tree Logic (TCTL), en udbredt forgrenet tidslogik. Meget arbejde med TCTL behandler ikke alle detaljer ved maksimale forløb; vi giver fuld semantik, inklusiv endelige maksimale forløb, som opstår ved deadlocks (fastlåsninger) og ved både strenge og ikke-strenge invarianter. Vi identificerer en klasse af oversættelser, der bevarer TCTL, og foreslår et generelt rammeværk til at bevise korrekthed af oversættelser mht. TCTL-formler. Nøglen er en én-til-mange-korrespondance: ét trin i kildesystemet kan simuleres af flere trin i målsystemet. Kan man etablere en sådan relation mellem tilstande, følger at oversættelsen bevarer enten hele TCTL eller kun sikkerhedsfragmentet, afhængigt af opfyldte krav. Rammeværket arbejder på niveauet af tidslige transitionssystemer og er dermed uafhængigt af den konkrete modelleringsformalism, hvilket gør det direkte anvendeligt for værktøjsudviklere (fx i værktøjer som UPPAAL, www.uppaal.com). For at demonstrere anvendeligheden udvikler vi to nye oversættelser fra TAPN til netværk af timed automata og beviser, at begge bevarer hele TCTL. Arbejdet er motiveret af den nylige udvikling i TAPAAL, hvor en oversættelse kun kunne håndtere liveness-egenskaber for en snæver klasse af TAPN-modeller (alle overgange med to indgående og to udgående buer). Efter vores bedste viden er vores oversættelser de første effektive oversættelser, der bevarer hele TCTL for vilkårlige begrænsede TAPN-modeller, og eksperimenter viser god praktisk ydeevne. Vi udvider desuden TAPN med heltalsvariabler, så tokens kan bære heltalsværdier, som kan bruges i tidsintervaller og invarianter. Vi introducerer også værdi-“guards” og værdiinvarianter, skitserer hvordan oversættelserne udvides til heltal, og konkluderer at korrektheden bevares. Implementeringen af oversættelserne samt støtte for inhibitorbuer og heltal er indarbejdet i en prototype af TAPAAL (www.tapaal.net), sammen med flere forbedringer.
Embedded software must meet strict timing requirements to ensure reliability and safety. Such systems are often modeled with time-aware formalisms like timed automata and time-extended Petri nets. This thesis studies Timed-Arc Petri Nets (TAPN), where tokens carry a real-valued age and arcs between places and transitions are guarded by time intervals that restrict which tokens may fire a transition. We extend the basic TAPN model with transport arcs, inhibitor arcs, and invariants, and we prove that invariants alone make the coverability and boundedness problems undecidable (i.e., no algorithm can decide them in all cases). We focus on formal verification (model checking) using Timed Computation Tree Logic (TCTL), a popular branching-time temporal logic. Much prior work does not handle all details of maximal runs; we give the full semantics, including finite maximal runs that arise with deadlocks and with both strict and non-strict invariants. We identify a class of translations that preserve TCTL and propose a general framework for proving correctness of translations with respect to TCTL formulae. The key idea is a one-by-many correspondence: one step in the source system can be simulated by several steps in the target system. If such a relation between states can be established, the translation preserves either the full TCTL or only the safety fragment, depending on the conditions met. Our framework operates at the level of timed transition systems, making it independent of the chosen modeling formalism and directly useful for tool developers (e.g., in tools like UPPAAL, www.uppaal.com). To illustrate applicability, we develop two novel translations from TAPN to networks of timed automata and prove that both preserve the full TCTL. This work is motivated by recent results in the TAPAAL tool, where a translation could handle only liveness properties on a narrow subclass of TAPN models (all transitions with two incoming and two outgoing arcs). To the best of our knowledge, our translations are the first efficient ones to preserve full TCTL for arbitrary bounded TAPN models, and experiments show good practical performance. We also add integer variables to TAPN, allowing tokens to carry integer values used in time intervals and invariants. We introduce value guards and value invariants, sketch how to extend our translations to handle integers, and conclude that correctness still holds. We implemented the translations and support for inhibitor arcs and integers in a prototype of the TAPAAL verification tool (www.tapaal.net), along with several improvements.
[This abstract was generated with the help of AI]
Keywords
Documents