{"id":4,"date":"2011-12-08T11:55:34","date_gmt":"2011-12-08T11:55:34","guid":{"rendered":"http:\/\/project.inria.fr\/template1\/?page_id=4"},"modified":"2013-05-23T13:03:19","modified_gmt":"2013-05-23T11:03:19","slug":"home","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/pyecdar\/","title":{"rendered":"About"},"content":{"rendered":"<p><\/p>\n<p style=\"text-align: justify;\">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.<\/p>\n<p style=\"text-align: justify;\">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:<\/p>\n<ul>\n<li>the computation of parallel composition and conjunction<\/li>\n<li>refinement checking<\/li>\n<li>consistency checking<\/li>\n<li>compatibility checking<\/li>\n<li>robust satisfaction checking<\/li>\n<li>robust consistency checking<\/li>\n<li>robust compatibility checking<\/li>\n<\/ul>\n<p>The tool implements its own engines:<\/p>\n<ul>\n<li>pytiga for timed games analysis and T-AdaCTL checking<\/li>\n<li>pyreachability for reachability and safety analysis<\/li>\n<li>pyrobustcegar for robustness analysis<\/li>\n<\/ul>\n<p>Additional algorithms are based on model transformations. Such transformations includes.<\/p>\n<ul>\n<li>parallel composition<\/li>\n<li>conjunction<\/li>\n<li>quotient<\/li>\n<li>consistency game<\/li>\n<li>compatibility game<\/li>\n<li>constant scaling<\/li>\n<li>robust game<\/li>\n<\/ul>\n<p>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 <a href=\"http:\/\/www.uppaal.org\/\">UPPAAL <\/a>format. The tools <a href=\"http:\/\/www.uppaal.org\/\">UPPAAL<\/a> or <a href=\"http:\/\/people.cs.aau.dk\/~adavid\/ecdar\/\">ECDAR<\/a>, can be used to edit these models.<\/p>\n<p><a name=\"people\"><\/a><\/p>\n<h1><span style=\"color: #e33729;\">People<\/span><\/h1>\n<p>PyECDAR is currently developped at INRIA Rennes.<\/p>\n<ul>\n<li><a href=\"http:\/\/people.irisa.fr\/Axel.Legay\/\">Axel Legay<\/a> is a researcher at and supervisor of the project.<\/li>\n<li><a href=\"http:\/\/people.rennes.inria.fr\/Louis-Marie.Traonouez\">Louis-Marie Traonouez<\/a> is a postdoc researcher and the lead developer of the project.<\/li>\n<li><a href=\"http:\/\/www.irisa.fr\/s4\/people\/ulrich.fahrenberg\/\">Uli Fahrenberg <\/a>is consultant for the project.<\/li>\n<\/ul>\n<p>PyECDAR was started at <a href=\"http:\/\/www.itu.dk\/\">IT University<\/a> under the supervision of <a href=\"http:\/\/www.itu.dk\/~wasowski\/\">Andrzej W\u0105sowski<\/a>. <a href=\"http:\/\/people.cs.aau.dk\/~pbulychev\/\">Peter Bulychev<\/a> is the developer of the first version of the timed game engine\u00a0used in PyECDAR.<\/p>","protected":false},"excerpt":{"rendered":"<p>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 &hellip; <\/p>\n<p><a class=\"more-link btn\" href=\"https:\/\/project.inria.fr\/pyecdar\/\">Continue reading<\/a><\/p>\n","protected":false},"author":1,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"open","template":"","meta":{"footnotes":""},"class_list":["post-4","page","type-page","status-publish","hentry","nodate","item-wrap"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/pyecdar\/wp-json\/wp\/v2\/pages\/4","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/pyecdar\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/project.inria.fr\/pyecdar\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/pyecdar\/wp-json\/wp\/v2\/users\/1"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/pyecdar\/wp-json\/wp\/v2\/comments?post=4"}],"version-history":[{"count":27,"href":"https:\/\/project.inria.fr\/pyecdar\/wp-json\/wp\/v2\/pages\/4\/revisions"}],"predecessor-version":[{"id":441,"href":"https:\/\/project.inria.fr\/pyecdar\/wp-json\/wp\/v2\/pages\/4\/revisions\/441"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/pyecdar\/wp-json\/wp\/v2\/media?parent=4"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}