Architecture

Inputs and outputs

architecture

The global architecture of PyECDAR with inputs and outputs is described in the figure above. In input the tool loads  models from XML files in the same format as Uppaal. The model is loaded in memory using symbolic representations for timing constraints (DBMs), feature expressions (BDDs) and parametric expression (Polyhedra). With the components loaded, the user can design the system to study using an algebra of operators between timed specifications. Then he can perform one or several queries in on demand manner that are processed by the engine.

The results output by the tool depend from the queries. For each timed game solved the tool computes a set of winning states. The allows for instance to synthesize the set of winning features that allows to satisfy a temporal formula. When checking for parametric robustness the tool computes the maximum value of the perturbation. Finally it can also save the models in a new XML file.

Source code structure

The source code of PyECDAR is separated in different modules:

  • pyecdar is the main interface of tool. It allows to load and save XML files. It defines a structure for specifications and it processes all the queries of the user by calling the adequate engine.
  • pynta defines the internal data structure for TIOA.
  • pyparamnta extends the structure with parametric constraints.
  • pysymbolicsates defines symbolic states, composed by a DBM and a BDD, union of symbolic states, and discrete states, composed by a location and values for integer variables.
  • pytadactl is a parser for T-AdaCTL formulae
  • pytiga contains all the timed games algorithms used in the tool. This includes:
    • Games algorithms from [CLST13] for adaptive systems that check T-AdaCTL formulae.
    • Safety game algorithm form [CDFLL05] for timed specifications.
    • Parametric refinement of strategies for parametric robustness from [Tra12].
  • pyreachability contains an implementation of the forward reachability (or safety) algorithm and an algorithm to parametrically refines counter-example. This used for refinement checking and parametric robust satisfaction checking.
  • pyrobustcegar contains the CEGAR algorithm for parametric robustness problems from [Tra12].
  • model_transformations contains functions to transform TIOA models. This includes:
    • Applying a perturbation to an implementation.
    • Computing the parallel composition, the conjunction, the quotient, of two specifications.
    • Computing the robust game automaton to perform robustness analysis from [LLTW11].
    • Preparing a specification to check consistency or compatibility.
  • misc_functions additional miscellaneous functions.