Wyniki wyszukiwania - BazTech

1

Distributed Timed Automata with Independently Evolving Clocks

Akshay S., Bollig B., Gastin P., Mukund M., Kumar K. N.

Fundamenta Informaticae

|

2014

|

Vol. 130, nr 4

377--407

EN

We propose a model of distributed timed systems where each component is a timed automaton with a set of local clocks that evolve at a rate independent of the clocks of the other components. A clock can be read by any component in the system, but it can only be reset by the automaton it belongs to. There are two natural semantics for such systems. The universal semantics captures behaviors that hold under any choice of clock rates for the individual components. This is a natural choice when checking that a system always satisfies a positive specification. To check if a system avoids a negative specification, it is better to use the existential semantics—the set of behaviors that the system can possibly exhibit under some choice of clock rates. We show that the existential semantics always describes a regular set of behaviors. However, in the case of universal semantics, checking emptiness or universality turns out to be undecidable. As an alternative to the universal semantics, we propose a reactive semantics that allows us to check positive specifications and yet describes a regular set of behaviors.

2

Blending Timed Formal Models with Clock Transition Systems

Jard C., Lime D., Roux O.H.

Fundamenta Informaticae

|

2014

|

Vol. 129, nr 1/2

85--100

EN

Networks of Timed Automata (NTA) and Time Petri Nets (TPNs) are well-established formalisms used to model, analyze and control industrial real-time systems. The underlying theories are usually developed in different scientific communities and both formalisms have distinct strong points: for instance, conciseness for TPNs and a more flexible notion of urgency for NTA. The objective of the paper is to introduce a new model allowing the joint use of both TPNs and NTA for the modeling of timed systems. We call it Clock Transition System (CTS). This new model incorporates the advantages of the structure of Petri nets, while introducing explicitly the concept of clocks. Transitions in the network can be guarded by an expression on the clocks and reset a subset of them as in timed automata. The urgency is introduced by a separate description of invariants. We show that CTS allow to express TPNs (even when unbounded) and NTA. For those two classical models, we identify subclasses of CTSs equivalent by isomorphism of their operational semantics and provide (syntactic) translations. The classical state-space computation developed for NTA and then adapted to TPNs can easily be defined for general CTSs. Armed with these merits, the CTS model seems a good candidate to serve as an intermediate theoretical and practical model to factor out the upcoming developments in the TPNs and the NTA scientific communities.

3

A Translation of the Existential Model Checking Problem from MITL to HLTL

Woźna-Szcześniak B., Zbrzezny A.

Fundamenta Informaticae

|

2013

|

Vol. 122, nr 4

401--420

EN

In the paper we propose a translation of the existential model checking problemfor timed automata and properties expressible in MITL to the existential model checking problem for HLTL. Such a translation, for example, allows to adopt LTL bounded model checking method for verification of the MITL properties

4

Runtime Monitoring of Contract Regulated Web Services

Lomuscio A., Penczek W., Solanki M., Szreter M.

Fundamenta Informaticae

|

2011

|

Vol. 111, nr 3

339-353

EN

We investigate the problem of locally monitoring contract regulated behaviours in agentbased web services. We encode contract clauses in service specifications by using extended timed automata. We propose a non intrusive local monitoring framework along with an API to monitor the fulfillment (or violation) of contractual obligations. A key feature of the framework is that it is fully symbolic thereby providing a scalable solution to monitoring. At runtime execution steps generated by the service are passed as input to the runtime monitor. Conformance of the execution against the service specification is checked using a symbolically represented extended timed automaton. This allows us to monitor service behaviours over large state spaces generated by multiple, long running contracts. We illustrate our methodology by monitoring a service composition scenario from the vehicle repair domain, and report on the experimental results.

5

Verification of FlexRay start-up mechanism by timed automata

Malinský J., Novák J.

Metrology and Measurement Systems

|

2010

|

Vol. 17, nr 3

461-480

EN

This contribution deals with the modelling of a selected part of a new automotive communication standard called FlexRay. In particular, it focuses on the mechanism ensuring the start-up of a FlexRay network. The model has been created with the use of timed automata and verified. For this purpose the UPPAAL software tool has been used that allows the modelling of discrete event systems with the use of timed automata, and subsequently the verification of the model with the use of suitable queries compiled in the so called computation tree logic. This model can be used to look for incorrect settings of time parameters of communication nodes in the network that prevent network start-up and subsequently the start of the car. The existence of this model also opens the way for finding possible errors in the standard. On the basis of the model, the work gives a case study of the start-up mechanism behaviour verification in a FlexRay network consisting of three communication nodes.

6

Undecidability Results for Timed Automata with Silent Transitions

Bouyer P., Haddad S., Reynier P-A.

Fundamenta Informaticae

|

2009

|

Vol. 92, nr 1-2

1-25

EN

In this work, we study decision problems related to timed automata with silent transitions (TAε) which strictly extend the expressiveness of timed automata (TA). We first answer negatively a central question raised by the introduction of silent transitions: can we decide whether the language recognized by a TAε can be recognized by some TA? Then we establish in the framework of TAε some old open conjectures that O. Finkel has recently solved for TA. His proofs follow a generic scheme which relies on the fact that only a finite number of configurations can be reached by a TA while reading a timed word. This property does not hold for TAε , the proofs in the framework of TAε thus require more elaborated arguments. We establish undecidability of complementability, minimization of the number of clocks, and closure under shuffle. We also show these results in the framework of infinite timed languages.

7

Universality Analysis for One-Clock Timed Automata

Abdulla P.A., Deneux J., Ouaknine J., Quaas K., Worrell J.

Fundamenta Informaticae

|

2008

|

Vol. 89, nr 4

419-450

EN

This paper is concerned with the universality problem for timed automata: given a timed automaton A, does A accept all timed words? Alur and Dill have shown that the universality problem is undecidable if A has two clocks, but they left open the status of the problem when A has a single clock. In this paper we close this gap for timed automata over infinite words by showing that the one-clock universality problem is undecidable. For timed automata over finite words we show that the one-clock universality problem is decidable with non-primitive recursive complexity. This reveals a surprising divergence between the theory of timed automata over finite words and over infinite words. We also show that if ε-transitions or non-singular postconditions are allowed, then the one-clock universality problem is undecidable over both finite and infinite words. Furthermore, we present a zone-based algorithm for solving the universality problem for single-clock timed automata. We apply the theory of better quasi-orderings, a refinement of the theory of well quasi-orderings, to prove termination of the algorithm. We have implemented a prototype tool based on our method, and checked universality for a number of timed automata. Comparisons with a region-based prototype tool confirm that zones are a more succinct representation, and hence allow a much more efficient implementation of the universality algorithm.

8

Translation of Timed Promela to Timed Automata with Discrete Data

Nabiałek W., Janowska A., Janowski P.

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

409-424

EN

The aim of the work is twofold. In order to face the problem of modeling time constraints in Promela, a timed extension of the language is presented. Next, timed Promela is translated to timed automata with discrete data, that is timed automata extended with integer variables. The translation enables verification of Promela specifications via tools accepting timed automata as input, such as VerICS or Uppaal. The translation is illustrated with a well known example of Fischer's mutual exclusion protocol. Some experimental results are also presented.

9

Translation of Intermediate Language to Timed Automata with Discrete Data

Janowska A., Janowski P., Wróblewski D.

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

235-248

EN

The aim of this work is to describe the translation from Intermediate Language, one of the input formalisms of the model checking platform VerICS, to timed automata with discrete data and to compare it with the translation to classical timed automata. The paper presents syntax and semantics of both formalisms, the translation rules as well as a simple example.

10

Towards Verification of Java Programs in VerICS

Zbrzezny A., Woźna B.

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

533-548

EN

VerICS is a tool for the automated verification of timed automata and protocols written in both the Intermediate Language and the specification language Estelle. Recently, the tool has been extended to work with Timed Automata with Discrete Data and with multi-agent systems. This paper presents a prototype Timed Automata with Discrete Data model of Java programs. In addition, we show how to use the model together with the verification core of VerICS to validate the well-known alternating bit protocol written in Java. # Greedy Algorithm for Attribute Reduction

11

SAT-based Unbounded Model Checking of Timed Automata

Penczek W., Szreter M.

Fundamenta Informaticae

|

2008

|

Vol. 85, nr 1-4

425-440

EN

We present an improvement to the SAT-based Unbounded Model Checking (UMC, for short) algorithm [13]. Our idea consists in building blocking clauses of literals corresponding not only to propositional variables encoding states, but also to more general subformulas over these variables encoding sets of states. This way our approach alleviates an exponential blow-up in the number of blocking clauses. A hybrid algorithm for verifying Timed Automata is proposed, where the timed part of blocking clauses is computed using Difference Bound Matrices. The optimization results in a considerable reduction in the size and the number of generated blocking clauses, thus improving the overall performance. This is shown on the standard benchmark of Fischer's Mutual Exclusion protocol.

12

Classes of Timed Automata and the Undecidability of Universality

Moura A.V., Pinto G.A.

Fundamenta Informaticae

|

2008

|

Vol. 82, nr 1-2

171-184

EN

Universality for deterministic Timed Büchi Automata (TBA) is PSPACE-complete but becomes highly undecidable when unrestricted nondeterminism is allowed. More precisely, universality for nondeterministic TBA is P11-hard and its precise position in the analytical hierarchy is still an open question. In this paper we introduce two types of syntactical restrictions to nondeterministic TBA, which are of independent interest, and show that their universality problem is P11-complete. These restrictions define, as we prove, proper subclasses of the class of timed languages defined by nondeterministic TBA. This suggests, as we argue, that no solution to that open question will come without surprise. We also establish closure properties and the relationships between the classes of languages we describe.

13

SAT-Based Reachability Checking for Timed Automata with Discrete Data

Zbrzezny A., Półrola A.

Fundamenta Informaticae

|

2007

|

Vol. 79, nr 3-4

579-593

14

Path Compression in Timed Automata

Janowska A., Penczek W.

Fundamenta Informaticae

|

2007

|

Vol. 79, nr 3-4

379-399

EN

The paper presents a method of abstraction for timed systems. To extract an abstract model of a timed system we propose to use static analysis, namely a technique called path compression. The idea behind the path compression consists in identifying a path (or a set of paths) on which a process executes a sequence of transitions that do not influence a property being verified, and replacing this path with a single transition. The method is property driven since it depends on a formula in question. The abstraction is exact with respect to all the properties expressible in the temporal logic CTL*-X.

15

Timed concurrent state machines

Daszczuk W. B.

Computer Science

|

2007

|

Vol. 8, Spec. Ed

23-36

EN

Timed Concurrent State Machines are an application of Alur Timed Automata concept to coincidence-based (rather than interleaving) CSM modeling technique. TCSM support the idea of testing automata, allowing to specify time properties easier than temporal formulas. Also, calculation of a global state space in real-time domain (Region Concurrent State Machines) is defined, allowing to storę a verified system in ready-to-verification form, and to multiply it by various testing automata.

PL

Współbieżne maszyny stanowe z czasem TCSM są aplikacją automatów czasowych Alura w środowisku koincydencyjnym współbieżnych maszyn czasowych CSM (w przeciwieństwie do środowisk przeplotowych). TCSM pasują do idei automatów testujących, które pozwalają wyspecyfikować zależności czasowe łatwiej niż poprzez formuły temporalne. Ponadto zdefiniowano sposób wyznaczania globalnej przestrzeni stanów w dziedzinie czasu (współbieżne maszyny stanowe regionów RCSM), co pozwala przechowywać badany system w postaci gotowej do weryfikacji i mnożyć go przez różne automaty testujące.

16

Slicing of Timed Automata with Discrete Data

Janowska A., Janowski P.

Prace Instytutu Podstaw Informatyki Polskiej Akademii Nauk

|

2006

|

Nr 990

1-29

EN

The paper proposes how to use static analysis to extract an abstract model of a system. The method uses techniques of program slicing to examine syntax of a system modeled as a set of timed automata with discrete data, a common input formalism of model checkers dealing with time. The method is property driven. The abstraction is exact with respect to all properties expressed in the temporal logic CTL_X*

PL

Praca przedstawia zastosowanie analizy statycznej do uzyskania abstrakcyjnego modelu systemu. Proponowana metoda jest oparta na technice plastrowania programów. Analizie podlega system przedstawiony jako zbiór automatów czasowych rozszerzonych o dane dyskretne, który to formalizm jest stosowany przez weryfikatory modelowe dla systemów czasowych. W przedstawionej metodzie abstrakcja systemu zachowuje prawdziwość formuł logiki temporalnej CTL_X* i jest uzalezniona od weryfikowanej własności.

17

Recognition of actions in meeting videos using timed automata

Pelc L., Kwolek B.

Machine Graphics and Vision

|

2006

|

Vol. 15, No. 3/4

577-584

EN

This paper addresses the problem of action recognition in meeting videos. A declarative knowledge provided graphically by the user together with person positions extracted by a tracking algorithm are used to generate the data for recognition. The actions have been formally specified using timed automata. The specification was verified on the basis of simulation tests as well as an analysis. The tracking is accomplished using a particle filter built on cues such as color, gradient and shape.

18

Slicing of Timed Automata with Discrete Data

Janowska A., Janowski P.

Fundamenta Informaticae

|

2006

|

Vol. 72, nr 1-3

181-195

EN

The paper proposes how to use static analysis to extract an abstract model of a system. The method uses techniques of program slicing to examine syntax of a system modeled as a set of timed automata with discrete data, a common input formalism of model checkers dealing with time. The method is property driven. The abstraction is exact with respect to all properties expressed in the temporal logic CTL_X*.

19

Slicing Timed Systems

Janowska A., Janowski P.

Fundamenta Informaticae

|

2004

|

Vol. 60, nr 1-4

187--210

EN

This paper presents a method of slicing timed systems to create reduced models for model checking verification. The reduction is made at the very beginning of the verification process and this makes it beneficial and effective in handling the state explosion problem. The method uses techniques of static analysis to examine the syntax of a program and to remove irrelevant fragments of the code. The timed extension of the classical slicing definition is given and applied to Intermediate Language of the verification system Verics and Estelle specification language.

20

Minimization Algorithms for Time Petri Nets

Półrola A., Penczek W.

Fundamenta Informaticae

|

2004

|

Vol. 60, nr 1-4

307--331

EN

The paper presents three methods for applying partitioning algorithms, used for generating abstract models for timed automata, to the case of time Petri nets. Each of these methods is based on a different approach to the concrete semantics of a net, and can potentially be more efficient than the others in a particular case. Besides the theoretical description, we provide some preliminary experimental results, obtained from the implementation integrated with the model checking tool VeriCS.