About

PyECDAR is a free software that analyses timed games and timed specifications. The tool allows to solve timed games based on timed automata models. These can be extended with adaptive features to represent dynamicity and model software product lines. The tool implements original algorithms for solving Timed AdaCTL formulae.

Timed specifications allow compositional reasoning between components based on Timed I/O Automata (TIOA). PyECDAR implements algorithms for the analysis of timed specifications. It includes in particular original methods for robustness analysis. The current features allow:

  • the computation of parallel composition and conjunction
  • refinement checking
  • consistency checking
  • compatibility checking
  • robust satisfaction checking
  • robust consistency checking
  • robust compatibility checking

The tool implements its own engines:

  • pytiga for timed games analysis and T-AdaCTL checking
  • pyreachability for reachability and safety analysis
  • pyrobustcegar for robustness analysis

Additional algorithms are based on model transformations. Such transformations includes.

  • parallel composition
  • conjunction
  • quotient
  • consistency game
  • compatibility game
  • constant scaling
  • robust game

The interface of the tool is designed for a python console. The user can load a TIOA model in the UPPAAL format, design the system by combining the processes using a simple algebra, transform the system, save it, and performs the analysis previously listed. The tool does not feature a GUI interface. It loads models from XML files in the UPPAAL format. The tools UPPAAL or ECDAR, can be used to edit these models.

People

PyECDAR is currently developped at INRIA Rennes.

PyECDAR was started at IT University under the supervision of Andrzej Wąsowski. Peter Bulychev is the developer of the first version of the timed game engine used in PyECDAR.