Wyniki wyszukiwania - BazTech

1

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.

2

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.

3

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*.

4

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.