Version 2.1 of PyECDAR has been released in the Download section.

This version fixes some bugs in prior version. In particular it uses to a new version of PyPPL in which compatibily issues between PyPPL and PyDBM have been resolved.

PyECDAR will be presented in a tool demonstration paper at the next ATVA conference (11th International Symposium on Automated Technology for Verification and Analysis). It will take place in Hanoi from the 14th to the 18th October. The paper is entitled: “PyEcdar: towards open source implementation for timed systems”.

Version 2.0 of PyECDAR has been released in the Download section.

This version combines version 1.0 with the special version that was built to analyse adaptive systems. This version is now independent from other open-source project such as PyUPPAAL since it includes its own parsing modules. It includes additional features, such as handling constants and variables.

We have design a new version of PyECDAR for the analysis of adaptive featured real-time systems. This version is currently separated from the main version of pyecdar. It includes a new parser for UPPAAL models with features that replaces PyUPPAAL. Features are added as boolean arrays. 3 types of arrays may be used and declare in a template has follow:

• bool Fa[n], Fb[n];
  It declares an array Fa of n adaptive system features, and the corresponding array Fb to update these features.
  These features can be changed by output transitions.
• bool Fe[n], Ff[n];
  It declares an array Fe of n adaptive environment features, and the corresponding array Ff to update these features. These features can be changed by input transitions.
• bool Fs[n];
  It declares an array Fs of n non adaptive system features. These features cannot be changed at runtime initialisation.

Features variable Fa[i], Fe[i] or Fs[i] can used in guards and invariants. The updates Fb[i] or Ff[i] can be used in guards only. These features expressions may only be used at then end of a guard (or an invariant) inside parentheses.  For instance the following guard:
(Fs[1] and ((Fa[0] and Fb[0]) or (not Fa[0] and not Fb[0])))
specifies that the transition is enable if the system feature Fs[1] is enable and that the adaptive feature Fa[0] is not altered by the transition. The last part can be shorten by using an assignment:

(Fb[0]=Fa[0])

You can have a look at the demo included in the package to see how to use this new version of PyECDAR.

In the future we will merge this version with the main version of PyECDAR.

Version 1.0 of PyECDAR has been released in the Download section.

The website of PyECDAR has been recently updated.

Documentation has been added about the the installation, the tool usage, based on a small tutorial, and some bibliography about timed specifications and robustness in timed specifications.

Some examples have also been added.

This is the new website for the tool PyECDAR. It will promote and distribute the tool, provide updates and documentation.

The old website of the tool was hosted on launchpad. This version will not be updated from now.