{"id":234,"date":"2012-12-19T15:07:21","date_gmt":"2012-12-19T14:07:21","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=234"},"modified":"2015-06-19T16:37:22","modified_gmt":"2015-06-19T14:37:22","slug":"languages","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/documentation\/languages\/","title":{"rendered":"Languages"},"content":{"rendered":"<p>PLASMA Lab uses two types of data,\u00a0 <strong>models<\/strong> and <strong>requirements<\/strong>. Given a model, PLASMA Lab will generate a large number of execution traces and will check the validity of a property for each one of these traces.<\/p>\n<p>On these pages you will find details on these languages. You could also take at look at our <a href=\"http:\/\/project.inria.fr\/plasma-lab\/Examples\">examples<\/a> collection.<\/p>\n<hr \/>\n<h3>Model<\/h3>\n<p>In its current version, PLASMA Lab is bundled with three model languages:<\/p>\n<ul>\n<li>Reactive Module Language (RML) of the PRISM tool, which is a popular probabilistic model checker tool supporting a wide rang of models. More documentation on this language can be found on <a href=\"http:\/\/www.prismmodelchecker.org\/\">PRISM web site<\/a>.<\/li>\n<li><a title=\"Adaptive Reactive Module Language\" href=\"https:\/\/project.inria.fr\/plasma-lab\/documentation\/languages\/model-languages\/\">Adaptive Reactive Module Language <\/a>is an extension of RML for adaptive systems.<\/li>\n<li><a href=\"https:\/\/project.inria.fr\/plasma-lab\/documentation\/languages\/rml-with-importance-sampling\/\">RML with importance sampling<\/a> for rare events simulation.<\/li>\n<li><a title=\"Biological language\" href=\"https:\/\/project.inria.fr\/plasma-lab\/documentation\/languages\/biological-language\/\">Biological Language<\/a><\/li>\n<\/ul>\n<p>Additionally, two plugins that can be downloaded from the <a title=\"Plugins\" href=\"https:\/\/project.inria.fr\/plasma-lab\/download\/plugins\/\">plugins page<\/a> allow to interface PLASMA Lab with MATLAB and SystemC:<\/p>\n<ul>\n<li><a href=\"https:\/\/project.inria.fr\/plasma-lab\/matlabsimulink\/\">MATLAB\/Simulink<\/a><\/li>\n<li><a href=\"https:\/\/project.inria.fr\/plasma-lab\/mag_manual\/\">SystemC\/MAG<\/a><\/li>\n<\/ul>\n<p>As we are using a modular architecture, you can develop your own model language and integrate it into Plasma Lab.<\/p>\n<hr \/>\n<h3>Requirements<\/h3>\n<p>Requirements languages also are modular. Plasma Lab comes with three:<\/p>\n<ul>\n<li><a title=\"Bounded Linear Temporal Logic\" href=\"https:\/\/project.inria.fr\/plasma-lab\/property-language\/\">Bounded-LTL<\/a><\/li>\n<li><a title=\"Bounded Linear Temporal Logic\" href=\"https:\/\/project.inria.fr\/plasma-lab\/property-language\/\">Adaptive BLTL<\/a><\/li>\n<li><a href=\"https:\/\/project.inria.fr\/plasma-lab\/gcsl\/ \">Goal Contract Specification Language<\/a><\/li>\n<\/ul>\n","protected":false},"excerpt":{"rendered":"<p>PLASMA Lab uses two types of data,\u00a0 models and requirements. Given a model, PLASMA Lab will generate a large number of execution traces and will check the validity of a property for each one of these traces. On these pages you will find details on these languages. You could also\u2026<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/plasma-lab\/documentation\/languages\/\"><span>Continue reading<\/span><i class=\"crycon-right-dir\"><\/i><\/a> <\/p>\n","protected":false},"author":234,"featured_media":0,"parent":130,"menu_order":0,"comment_status":"closed","ping_status":"open","template":"","meta":{"footnotes":""},"class_list":["post-234","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/234","targetHints":{"allow":["GET"]}}],"collection":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages"}],"about":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/types\/page"}],"author":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/users\/234"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/comments?post=234"}],"version-history":[{"count":55,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/234\/revisions"}],"predecessor-version":[{"id":2090,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/234\/revisions\/2090"}],"up":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/130"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/media?parent=234"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}