{"id":1635,"date":"2014-12-10T18:48:19","date_gmt":"2014-12-10T17:48:19","guid":{"rendered":"https:\/\/project.inria.fr\/plasma-lab\/?page_id=1635"},"modified":"2016-01-25T11:51:18","modified_gmt":"2016-01-25T10:51:18","slug":"mag_manual","status":"publish","type":"page","link":"https:\/\/project.inria.fr\/plasma-lab\/documentation\/tutorial\/mag_manual\/","title":{"rendered":"SystemC Plugin"},"content":{"rendered":"<p>This manual shows how to use the <a href=\"https:\/\/project.inria.fr\/pscv\/\">SystemC Plugin and the MAG tool<\/a> in order to perform statistical model checking on SystemC models. Running the verification framework consists of two steps:<\/p>\n<ul>\n<li>Generating an executable model corresponding to the verifying properties with MAG tool,<\/li>\n<li>And using the SystemC plugin plugin to verify the properties.<\/li>\n<\/ul>\n<h2>Download<\/h2>\n<ul>\n<li>Monitor and Aspect-advice Generator <a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2015\/09\/MAG-1.0.tar_.gz\">MAG 1.0<\/a><\/li>\n<li>Aspect-oriented Programming with C\/C++\u00a0<a href=\"http:\/\/aspectc.org\/Download.php\">AspectC++ 1.2<\/a><\/li>\n<li>Patched version of SystemC in <a href=\"http:\/\/sourceforge.net\/projects\/chimp-rice\/\">CHIMP 1.0<\/a><\/li>\n<\/ul>\n<h2>Installation<\/h2>\n<p>To compile and install MAG, AspectC++ and the patched version of SystemC, refer to the<a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2015\/09\/MAG_UserGuide.pdf\"> MAG user guide<\/a>.<\/p>\n<p><span style=\"color: #333333; font-family: 'Pontano Sans', arial, sans-serif; font-size: 20px;\">Generating Executable Model with MAG<\/span><\/p>\n<p>In order to run the SystemC plugin to verify the properties, users first need to generate an executable model form the original SystemC model. It consists of three steps:<\/p>\n<ul>\n<li>Use MAG to generates the monitors and the aspect-advice file.<\/li>\n<li>Run AspectC++ with the generated aspect-advice file on the generated monitors and original model code to instrument the original model code.<\/li>\n<li>Compile (e.g., g++) the instrumented SystemC model code to produce the corresponding executable model<\/li>\n<\/ul>\n<p>Users run MAG to generate the monitors and aspect advices according to the verifying properties as follows:<\/p>\n<ul>\n<li>Write the configuration file according to the verifying properties (see the <a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2015\/09\/MAG_UserGuide.pdf\">MAG user guide<\/a> for more details)<\/li>\n<\/ul>\n<ul>\n<li>Change to the directory of the MAG tool and run\u00a0<em><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><\/em>mag -conf &#8220;configuration file&#8221;<em><\/div><\/em><\/li>\n<\/ul>\n<ul>\n<li>MAG generates three files: header and source files of the generated monitor, and the aspect advice file &#8220;aspect_definitions.ah&#8221; in the location defined in the configuration file<\/li>\n<\/ul>\n<p>Users run AspectC++ with the aspect-advice file on the original model source code and the generated monitors to generate the instrumented SystemC model.<\/p>\n<ul>\n<li>Change the directory of AspectC++ 1.2<\/li>\n<li>Run the following command to generate puma.config file in the working directory <em><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><\/em>ag++ &#8211;gen_config<em><\/div><\/em><\/li>\n<li>Copy the header and source files of the generated monitors and the aspect-advice file &#8220;aspect_definitions.ah&#8221; into the source directory of the original model source code<\/li>\n<li>For each header or source file of the SUV, run the following command to generate the instrumented version\u00a0<em><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><\/em>ac++ -c &#8220;source_path\/input_file&#8221; -o &#8220;target_path\/output_file&#8221; -p &#8220;source_path&#8221; -I &#8220;source_path&#8221; -I &#8220;systemc_path&#8221;\/include\u00a0&#8211;config &#8220;aspectc_path&#8221;\/puma.config<em><\/div><\/em>where &#8220;source_path&#8221;\u00a0is the path to the source directory of the original model source code, &#8220;target_path&#8221; is the path to the directory where the AspectC++ puts the instrumented version, &#8220;systemc_path&#8221; is the path to the patched version of systemc-2.3.0 (included in CHIMP), and &#8220;aspectc_path&#8221;\u00a0is the path to the AspectC++ 1.2.<\/li>\n<\/ul>\n<p>Compiling the instrumented model source code is done as follows:<\/p>\n<ul>\n<li>In the main header file , include the generated monitor header file, for example\u00a0<em><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><\/em>#include \u00a0&#8220;monitor_multi_lift.h&#8221;<em><\/div><\/em><\/li>\n<\/ul>\n<ul>\n<li>In the main source file, add the following line just before the call to sc_start()<em><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><\/em>mon_observer* obs = local_observer::createInstance(1, other_parameters);<em><\/div><\/em>The parameters depend on the generated monitor, for example, in the included example of multi-lift system in the MAG tool package, it is:<em><div class=\"alert alert-success\" role=\"alert\"><p class=\"printonly\"><strong>Important!<\/strong><\/p><\/em>mon_observer* obs\u00a0 =\u00a0 local_observer::createInstance(1, &amp;liftsystem);<em><\/div><\/em><\/li>\n<\/ul>\n<ul>\n<li>Compile the instrumented model source code with g++ compiler and link with the patched SystemC<\/li>\n<\/ul>\n<p>We also provide the shell scripts in the example directory of MAG tool that automatically generated the instrumented model source code. User can modify them according to his configuration and requirements.<\/p>\n<h2>Running SystemC Plugin with Plasma<\/h2>\n<p>After compiling the instrumented SystemC model, an executable model is produced. \u00a0Users then can verify the desired properties with the SystemC plugin of Plasma as follows:<\/p>\n<ul>\n<li>Launch Plasma Lab with the SystemC plugin, create a new project, then create a new model of the type &#8220;SystemC Specification&#8221;. The content of the model is the path to the executable model<\/li>\n<\/ul>\n<p><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/12\/Selection_005.png\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone  wp-image-1681\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/12\/Selection_005-300x207.png\" alt=\"Selection_005\" width=\"592\" height=\"413\" \/><\/a><\/p>\n<ul>\n<li>Write the verifying properties based on the observed variables that are available in the executable model as shown in the following figure (inside the red area)<\/li>\n<\/ul>\n<p><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/12\/Plasma-Lab_0011.png\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone  wp-image-1682\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/12\/Plasma-Lab_0011-300x208.png\" alt=\"Plasma Lab_001\" width=\"599\" height=\"424\" \/><\/a><\/p>\n<ul>\n<li>Check the properties as usual with Plasma Lab<\/li>\n<\/ul>\n<p><a href=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/12\/Plasma-Lab_002.png\"><img loading=\"lazy\" decoding=\"async\" class=\"alignnone  wp-image-1683\" src=\"https:\/\/project.inria.fr\/plasma-lab\/files\/2014\/12\/Plasma-Lab_002-300x208.png\" alt=\"Plasma Lab_002\" width=\"600\" height=\"420\" \/><\/a><\/p>\n","protected":false},"excerpt":{"rendered":"<p>This manual shows how to use the SystemC Plugin and the MAG tool in order to perform statistical model checking on SystemC models. Running the verification framework consists of two steps: Generating an executable model corresponding to the verifying properties with MAG tool, And using the SystemC plugin plugin to\u2026<\/p>\n<p> <a class=\"continue-reading-link\" href=\"https:\/\/project.inria.fr\/plasma-lab\/documentation\/tutorial\/mag_manual\/\"><span>Continue reading<\/span><i class=\"crycon-right-dir\"><\/i><\/a> <\/p>\n","protected":false},"author":525,"featured_media":0,"parent":135,"menu_order":0,"comment_status":"closed","ping_status":"closed","template":"","meta":{"footnotes":""},"class_list":["post-1635","page","type-page","status-publish","hentry"],"_links":{"self":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1635","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\/525"}],"replies":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/comments?post=1635"}],"version-history":[{"count":18,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1635\/revisions"}],"predecessor-version":[{"id":2165,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/1635\/revisions\/2165"}],"up":[{"embeddable":true,"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/pages\/135"}],"wp:attachment":[{"href":"https:\/\/project.inria.fr\/plasma-lab\/wp-json\/wp\/v2\/media?parent=1635"}],"curies":[{"name":"wp","href":"https:\/\/api.w.org\/{rel}","templated":true}]}}