MAG-1.0 User Manual
Contents
1. before value Using this trigger user can define a variabble that will contain the return value a parameter value passing to a function defined in the SystemC model Then user can use this variable to define his formula The syntax is given as follows value type_of variable name_of_variable function pattern i It defines a variable that contains the value passed as it i can be from 1 to the number of arguments the function has parameter to the function value type_of variable name_of_variable function_pattern 0 It defines a variable that contains the return value of the function formula The value of this trigger is a specification that contains two ele ments in the form BLT Lformula name The firt element is a BLTL formula and the second one is the name of the specification For example formula G lt 100 at gt 1 property_1 time resolution The user defined temporal resolution For example time_resolution MON_TIMED_NOTIFY_PHASE_END comment To make a line as a comment user puts at the beginning of the line then MAG will ignore it We also provide a dummy mm_config txt file in the source code directory of MAG User can modify it according to his requirements 5 BLTL and Clock Expressions User specifies the desired properties in bounded linear temporal logic formulas and the sampling rate of states in the execution traces by clock expressions BLTL is defined by the following grammar w2. primitives entry exit call and return that refer to the location immediately before the first executable statement the location immediately after the last executable statement in a function the location that contains the function call and the location immediately after the function call respectively The syntaxes of these primitives in the configuration file are given as follows location location variable name function_pattern entry location location variable name function_pattern exit location location variable name function_pattern call location location_variable name function pattern return where the function_pattern follows the same as pointcut expressions in As pectC The function_pattern has the form returntype class_name funtion_name argument_list plocation This trigger helps user define a Boolean variable that holds the value true immediately before or after the execution of all statements that match the value of the trigger defined as a regular expression The syntax of this trigger is plocation location variable name statement before or plocation location_variable name statement after For example we want to declare the Boolean variable locl that holds the value true immediately before the execution of all statements that contain the devision operator followed by zero of more spaces and the variable a We write the following trigger in the configuration file plocation locl x a
3. send_start producer send call location send_done producer send return Similarly the trigger location rcv Yoconsumer receive return declares a Boolean variable rcv that holds the value true immediately after a function call of the function receive of the module consumer Using these triggers the property is expressed as follows Gi send_start gt send_done U rcv arg_expr is an expression that uses the return values parameter values pass ing to functions defined in the SystemC model This expression can be formed by using the trigger value in the configuration file For each process name the primitive proc_expr indicates the status of this process in the simulator kernel that can be waiting runnable or running The kernel_expr consists of the primitives to expose the current state of the kernel phase_expr e g end of delta cycle notification and when a specific event is notified event_expr For instance the following trigger declares a Boolean variable wevent that holds immediately when write_event is notified eventclock wevent write_event noti fied This variable can be used to define a temporal resolution in the configuration file of our framework As explained earlier users can define their own temporal resolutions A tem poral resolution is specified by using a disjunction of events locations or kernel phases as in the BLTL formula of the form clk clkg For instance
4. MAG 1 0 User Manual Chan Ngo INRIA 35042 Rennes Cedex France Tool Name MAG Monitor and Aspect Generator Developed by Chan Ngo Owened by INRIA France Maintained by Chan Ngo chan ngo inria fr Realeased in October 2014 Description MAG is a tool for generating monitored versions of SystemC models in order to perform statistical model checking with Plasma Lab MAG is based on the techniques in the CHIMP tool by Sonali Dutta Deian Tabakov and Moshe Y Vardi Download https project inria fr plasma lab mag_manual Platform MAG can be installed and run in any unix environment e g Ubuntu Linux Mac OS License MAG uses GNU GPL Version 3 1 Components MAG consists of 3 following components MAG 1 0 This component is reponsible to automatically generate the mon itors and the aspect advice file for instrumentation in order to observe exe cution traces of the SystemC model AspectC 1 2 It is used by MAG to instrument the model under verification MUV SystemC 2 3 0 modified The patched version of OSCI kernel 2 3 0 The pat ach enables user defined temproal resolutions sampling rates during observ ing execution traces 2 Installing MAG To install and run MAG the following packages are required boost library autoconf 2 61 and later automake 1 10 and later libtool 2 4 and later GNU make 3 81 and later To install run make to compile MAG and run make cle
5. an to uninstall MAG In order to make the instrumented SystemC model run the modified version of SystemC is needed To install SystemC please refer to the INSTALL file in the provided SystemC package 3 Running MAG To run MAG users need to write a configuration file first containing all prop erties to be verified with the declarations of all used primitives as well as other necessary information From this configuration MAG generates the monitors and an aspect advice file that is then used by AspectC to generate the in strumented model Finally the instrumented MUV code and the monitor are compiled together and linked with the SystemC kernel into an executable model The executable model resulting from the first step is run through our plugin to execute the simulation with the inputs provided by users For every property Plasma lab checks the validity of the property according to the execution traces produced by the corresponding monitor 3 1 Generating Monitor with MAG User runs MAG to generate the monitor and aspect advices according to the property to be verified Write the configuration file according to the verifying property see Section 4 for more details Change to the directory of the MAG tool and run mag conf path to configuration file MAG will generate three files header and source files of the monitor and the aspect advice file aspect_definitions ah in the user defined location 3 2 Instrum
6. ded execution After an sc_thread has suspended Table 1 Predefined Kernel Phases 10 6 Contact Chan Ngo chan ngo inria fr INRIA Rennes 263 avenue du G n ral Leclerc 35042 Rennes France
7. enting with AspectC User runs AspectC with the MUV the generated monitor and the aspect advice file to instrument the MUV Change the working directory to AspectC 1 2 Run the following command to generate puma config file in the working directory ag gen config Copy the header and source of the generated monitor and the aspect advice file aspect definitions ah inside the source directory of the MUV For each header or source file of the MUV user runs the following command to generate the instrumented version ac c SOURCE HOME file name o TARGET_HOME file name p SOURCE HOME I SOURCE HOME I SYSTEMC_ HOME include config ASPECTCHOME puma con fig where SOURCE HOME is the path to the source directory of the MUV TARGET HOME is the path to the directory where user wants the As pectC puts the instrumented version SYSTEMC_HOME is the path to the patched version of systemc 2 3 0 and ASPECTC_HOME is the path to the AspectC Alternatively user can use the sheel script included in the examples to make the steps above automatically 3 3 Compiling Instrumented Code In the main header file of the MUV user includes the monitor header file for example include monitor multi lift h In the source file of the MUV user adds the following line just before the call to sc_start mon observer x obs local_observer createInstance 1 parameters The parameters depends o
8. here the time bound t that repre sents an amount of simulation time or a number of state changes in an execution trace in our verification framework it has the form lt number Y true falselp AP y A p2 p p1 Vr Ye The temporal modalities F the eventually sometimes in the future and G the always from now on forever can be derived from the until U as Fr trueU y and Gy AF 7y respectively The semantics of BLTL is defined w r t finite sequences of states of MM We denote the fact that w a finite sequence of states satisfies the BLTL formula y by w E g FE true and w j false ew e ut p p AP if and only if p L w k e w H p1 A g2 if and only if w 41 and w 2 e w H y if and only if w Ky e wf Uty if and only if there exists an integer i such that w t K wo Zicilt ti lt t and for each 0 lt J lt i wT F Y1 The set of atomic propositions AP that is formed by the primitives that are declared in the configuration file of our framework and let users define properties about the states of user code and SystemC kernel We have the following SystemC expr model_expr kernel_expr model_expr att_expr loc_expr arg expr proc_expr loc_expr before after code_label syntax_expr func name entry exit call return arg_expr func name nonnegative_integer proc_expr proc_name proc_state kernel_expr phase_expr event_expr phase_expr ker
9. n the generated monitor for example in the in cluded example of multi lift system in the MAG tool package it is mon_observer obs local_observer createInstance 1 amp liftsystem User compiles the instrumented MUV with g compiler and links with the patched SystemC libary provided in MAG package We also provide the shell scripts in the example directory of MAG tool that au tomatically generated the instrumented MUV User can modify them according to his requirements 4 Configuration File Triggers The configuration file is used to guide MAG generating the appropriate monitors and aspect advice file using by AspectC Its triggers are given as follows verbosity The integer value between 0 and 9 It represents the level of information messages outputing by MAG The default value is 1 For example to define the value of verbosity as 6 User can write verbosity 6 output file The path to the source file of the generating monitor By de fault MAG will generate a file monitor cc in the working directory of MAG For example output_file home user model my_monitor cc output_header_file The path to the header file of the generating moni tor The default header file is based on the name of the output_file without extension For example output_header_file home user model my monitor h mon_name The name of the generated monitor The default is monitor For example monname my_monitor plasma file The path t
10. nel_phase event_expr n event name notified att_expr is an expression that involves evaluations of variables including module s protected and private attributes User uses attribute trigger to form model_expr For example attribute m a a to observe the value of a in the module M given that the triggers usertype and type are defined as usertype M and type M x m respectively loc_expr is an expression that uses a location in the source code of the verify ing model which is defined using location and plocation triggers in the configura tion file For example assume that we want to specify the property always the value of the variable a in the module M is different from 0 whenever it is used as a divisor within t seconds We first define the trigger plocation locl xa before that declares the Boolean variable locl that holds the value true immediately before the execution of all statements that contain the devision operator followed by zero of more spaces and the variable a With the attribute above the property is expressed as follows G locl gt a 0 Another example assume that user wants to specify the property send remains blocked until receive has returned within t seconds The following triggers declare Boolean variables send_start and send_done that hold the value true immediately before and after a function call of the function send of the module producer respectively location
11. o the generated Plasma Lab project file For exam ple plasma_file home user PLASM A_Lab 1 3 0 my_project plasma plasma_project_name The generated Plasma Lab project name For ex ample plasma_project name my project plasma_model_name The Plasma Lab model For example plasma_model_name my_model plasma_model_content The path to the executable SystemC model For example plasma model content home user model instrumented muv write to file Write execution traces to a file For example user does not want to log the traces to file write_to_file false include If the verifying property uses references to an object of a class or a module Then this trigger indicates the header file that needs to be included in the header file of the monitor For example there is a reference to the module A that is declared in the header file A h then we define the include trigger as follows include A h usertype Consider an object of type class A user wants to refer to at tributes of this object These attributes can be protected private public or accessed by some getting methods To make the monitor generated by MAG can access these attributes user uses the usertype trigger as follows usertype A type If the verifying property uses references to an object of class or module of type T users need to tell MAG that this object has type T To do that user defines the value of type trigger For example consider a pro
12. perty that refers to two object pointers of types class A and B respectively Then user defines the trigger as follows type Axa type Bxb attribute The value of this trigger defines which attributes of an object that user wants to observe the values during the execution of the model The trigger syntax is attribute attribute name label For example assume that user wants to observe the value of the private attribute t of the above object pointer a of type class A and labels it with a t User can write attribute a tat att_type For each defined attribute user needs to define its type MAG sup ports all primitive datatypes of SystemC and C except char and string The trigger syntax is att_type type name attribute_label For example con sider the above attribute at assume that it is of type int User write the following trigger in the configuration file att_type int at eventclock The value of this trigger defines a Boolean variable that is true immediately when a specific event is notified This variable ussually is used to define a temporal resolution For example consider an event e of the object a The following Boolean variable e_noti fied is set to be true whenever e is notified eventclock a e notified e notified location The value of this trigger defines a Boolean variable that is true whenever a location in the source code model will arrive during the simula tion Location trigger provides four
13. the spec ification time resolution locl will check the formula over a trace of states sampled each time the location loc1 is reached If user provide no clock expression MAG will sample at all 18 predefined kernel phases Table 1 shows the list of 18 predefined kernel phases Phase name Sampling location MON MON MON MON MON MON MON MON MON MON MON MON MON MON MON MON MON MON INIT_PHASE BEGIN _INIT UPDATE PHASE BEGIN INIT UPDATE PHASE END _INIT DELTA NOTIFY PHASE _ BEGIN _INIT DELTA NOTIFY PHASE ENDS INIT PHASE END DELTA CYCLE BEGIN DELTA CYCLE END EVALUATE PHASE BEGIN _EVALUATE PHASE END _UPDATE PHASE BEGIN _UPDATE PHASE END DELTA NOTIFY PHASE BEGIN _DELTA NOITIFY PHASE END TIMED NOTIFY PHASE BEGIN TIMED NOTIFY PHASE END METHOD SUSPEND THREAD SUSPEND Before initialization phase begins Before initialization update phase begins After initialization update phase ends Before initialization delta notification phase begins After initialization delta notification phase ends After initialization phase ends Before a delta cycle begins After a delta cycle ends Before an evaluation phase begins After an evaluation phase ends Before an update phase begins After an update phase ends Before a delta notification phase begins After a delta notification phase ends Before a timed notification phase begins After a timed notification phase ends After an sc_method has en
Download Pdf Manuals
Related Search