TReX and IF

Type

lecture

Language

English

Authors

Matoušek Petr, doc. Ing., Ph.D., M.A. (DIFS)

URL

http://www.fit.vutbr.cz/~matousp/doc/2005/trex-intro.pdf

Keywords

parametric analysis, timed model-checker, TReX

Abstract

TReX is a tool for automatic analysis and model checking of timed systems with parameters. Models are based on extended timed automata. During analysis, TReX generates a set of reachable configurations, that can be later processed by CADP or SMV while finite model-checking. In addition, it perfoms on-the-fly checking of safety properties.

In this talk we introduced basic features of TReX, input language IF and some background of implementation based on parametric DBMs. Several examples of parametric model checking will be showed.

Annotation

TReX is a tool for automatic analysis and model checking of timed systems with parameters. Models are based on extended timed automata. During analysis, TReX generates a set of reachable configurations, that can be later processed by CADP or SMV while finite model-checking. In addition, it perfoms on-the-fly checking of safety properties.

In this talk we introduced basic features of TReX, input language IF and some background of implementation based on parametric DBMs. Several examples of parametric model checking will be showed.

Published

2005

Pages

38

Place

ParaDiSe seminary, FI MU Brno

BibTeX

@misc{BUT64632,
  author="Petr {Matoušek}",
  title="TReX and IF",
  year="2005",
  pages="38",
  address="ParaDiSe seminary, FI MU Brno",
  url="http://www.fit.vutbr.cz/~matousp/doc/2005/trex-intro.pdf",
  note="lecture"
}