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:
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 and ((Fa and Fb) or (not Fa and not Fb)))
specifies that the transition is enable if the system feature Fs is enable and that the adaptive feature Fa is not altered by the transition. The last part can be shorten by using an assignment:
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.