{"id":16,"date":"2016-05-31T11:07:34","date_gmt":"2016-05-31T11:07:34","guid":{"rendered":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/?page_id=16"},"modified":"2016-11-20T10:19:06","modified_gmt":"2016-11-20T10:19:06","slug":"real-time-studio","status":"publish","type":"page","link":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/real-time-studio\/","title":{"rendered":"Real time Studio"},"content":{"rendered":"<p><img loading=\"lazy\" decoding=\"async\" class=\"size-medium wp-image-17 alignright\" src=\"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-content\/uploads\/sites\/548\/2016\/05\/graphlab5-300x189.jpg\" alt=\"graphlab5\" width=\"300\" height=\"189\" srcset=\"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-content\/uploads\/sites\/548\/2016\/05\/graphlab5-300x189.jpg 300w, http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-content\/uploads\/sites\/548\/2016\/05\/graphlab5.jpg 350w\" sizes=\"auto, (max-width: 300px) 100vw, 300px\" \/><\/p>\n<p><strong>Real Time Studio<\/strong> (RT-Studio) is an integrated environment for the edition, simulation and automatic verification of real time systems modeled as networks of Interpreted Time Petri Nets (ITPNs). In its current version the tool proposes the construction of several abstractions for ITPNs suitable to verify their reachability, linear and branching properties. RT-Studio also integrates a classical CTL model-checker, an innovative TCTL model-checker based on a forward on the fly verification technique, and a minimizer under bisimulation. The environment is also intended as a general purpose simulation an verification tool for other extensions of Petri nets as it already allows to construct and simulate Interpreted Hybrid Functional Petri Nets (IHFPNs) for Biopathways analysis and continuous event system simulation. Other extension to the tool are also expected to support colored Petri nets and timed automata.<\/p>\n<p>Last update: 07\/05\/2014<\/p>\n<p>Download (windows version): <a href=\"https:\/\/www.dropbox.com\/s\/izawhjhv3uspqm4\/RT-Studio-win-v1.17.zip?dl=0\">RT-Studio-win-v1.17.zip<\/a><\/p>\n<p>To install, unzip &#8216;RT-Studio-win-v#.zip&#8217; in a directory of your choice.<br \/>\nTo run, double click\u00a0 RT-Studio.jar.<\/p>\n<p>For any feedback please contact Dr. Rachid Hadjidj (<a href=\"mailto:rhadjidj@qu.edu.qa\">rhadjidj@qu.edu.qa<\/a>) or Dr. Hanifa Boucheneb (<a href=\"mailto:hanifa.boucheneb@polymtl.ca\">hanifa.boucheneb@polymtl.ca<\/a>).<\/p>\n<p><strong>Video tutorials:<\/strong><\/p>\n<ol>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/d662i8enw94vlb5\/RT-Studio-Installation.wmv?dl=0\">Installation instructions<\/a><\/li>\n<li>Tool overview\n<ol>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/hbp6ot9j29rh7zv\/creating_a_petrinet.wmv?dl=0\">A\u00a0simple TPN<\/a><\/li>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/0tmvc44r2huwuti\/interpretedpetrinet.wmv?dl=0\">A\u00a0simple Interpreted TPN<\/a><\/li>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/ub17vdwj8rd53h9\/placesyn.wmv?dl=0\">Synchronizing Project components using places<\/a><\/li>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/2n2lyb1m52mp5r4\/transitionsyn.wmv?dl=0\">Synchronizing Project components using transitions<\/a><\/li>\n<\/ol>\n<\/li>\n<li>TCTL verification (comming very soon)<\/li>\n<li>State spaces generation (comming very soon)<\/li>\n<li>HFPN simulation (comming very soon)<\/li>\n<li><a href=\"https:\/\/www.dropbox.com\/s\/elgij78e6agzisj\/uppaalcomparison.wmv?dl=0\">A comparison with UPPAAL<\/a><\/li>\n<\/ol>\n<p><img loading=\"lazy\" decoding=\"async\" class=\"alignnone wp-image-18\" src=\"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-content\/uploads\/sites\/548\/2016\/05\/rt-studio-300x188.png\" alt=\"rt-studio\" width=\"895\" height=\"561\" srcset=\"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-content\/uploads\/sites\/548\/2016\/05\/rt-studio-300x188.png 300w, http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-content\/uploads\/sites\/548\/2016\/05\/rt-studio-768x480.png 768w\" sizes=\"auto, (max-width: 895px) 100vw, 895px\" \/><\/p>\n","protected":false},"excerpt":{"rendered":"<p>Real Time Studio (RT-Studio) is an integrated environment for the edition, simulation and automatic verification of real time systems modeled [&hellip;]<\/p>\n","protected":false},"author":530,"featured_media":0,"parent":0,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-16","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-json\/wp\/v2\/pages\/16","targetHints":{"allow":["GET"]}}],"collection":[{"href":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-json\/wp\/v2\/users\/530"}],"replies":[{"embeddable":true,"href":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-json\/wp\/v2\/comments?post=16"}],"version-history":[{"count":11,"href":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-json\/wp\/v2\/pages\/16\/revisions"}],"predecessor-version":[{"id":98,"href":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-json\/wp\/v2\/pages\/16\/revisions\/98"}],"wp:attachment":[{"href":"http:\/\/qufaculty.qu.edu.qa\/rhadjidj\/wp-json\/wp\/v2\/media?parent=16"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}