Documentation

• boost library
• autoconf 2.61 and later
• automake 1.10 and later
• libtool 2.4 and later
• GNU make 3.81 and later
• Java SDK or JRE 1.6 and later
• g++ with build-essential package
• libpuma-dev package used by AspectC++
• GNU Scientific Library 1.6 and later for running the example code

Unzip the archive pscv.tar.gz into a directory of your choice. There are the following sub-folders:

• mag : MAG source program for generating the C++ monitor and aspect advices for AspectC++
• systemc-2.3.0_modified : the patch version of SystemC-2.3.0 with random scheduler implementation
• aspectc++ : Linux/x86-64bit binary version of AspectC++
• examples : some example code
• docs : User Guide for installing and writing configuration file for MAG

To compile PSCV from source, in the top folder, run the following commands:

 make

The program mag and dynamic library of patch SystemC will be in folders mag and systemc-2.3.0_modified/lib-linux64 (if you comppile for Linux/x86-64bit), respectively.

In the aspectc++ folder (you should download a suitable version of AspectC++ for your architecture), make AspectC++ runnable by running the commands:

chmod +x aspectc++/ag++

chmod +x aspectc++/ac++

Finally, add the path to dynamic library of SystemC to LD_LIBRARY_PATH, for example,

export LD_LIBRARY_PATH=/home/username/pscv/systemc-2.3.0_modified/lib-linux64:$LD_LIBRARY_PATH

To uninstall, in the top folder, simply run the command:

make clean

Alternatively, you can compile separately each components of PSCV as follows. Go to mag folder and run

make

Go to systemc-2.3.0_modified and run the followings commands:

mkdir objdir 

cd ./objdir 

export CXX=g++

../configure

make

make install

2. Verification flow

The verification flow using PSCV consists of the three steps as depicted in the following figure, see the MAG user guide for the full syntax and semantics of language for writing a configuration file:

1. In the first step, users write a configuration file containing a set of typed variables called observed variables, a Boolean expression called temporal resolution, and all properties to be verified. MAG translates the configuration file into a C++ monitor, a set of aspect-advices, and/or the corresponding Plasma Lab project file.
2. Use AspectC++ to automatically instrument the MUV along with the generated monitor and aspect-advice file to expose the user model’s state and syntax in the second step. The instrumented model and the generated monitor are compiled and linked together with the modified SystemC kernel, i.e., with GCC, into an executable model.
3. Launch Plasma Lab with the SystemC plugin put in the “plugins” folder, then open the generated Plasma Lab project file to verify the interested properties in Plasma Lab as usual.

3. A running example

We provide some shell script templates for generating monitor, aspect-advice files and instrumenting the MUV code with AspectC++. For example, to run the producer and consumer example code. All examples except the random scheduler, the structure of the source code is:

• src : the source code of the example, including a configuration file named mm_config.txt
• ins : output folder for instrumented code from AspectC++, including a provided Makefile template
• gen : C++ monitor, aspect-advice, and Plasma Lab project files output folder from MAG
• mag_run.sh : a provided bash shell script template for running MAG tool
• aspectc++_run.sh: a provided bash shell script template for running AspectC++ tool

The running contains the following steps:

•  In the src folder, modify the file mm_config.txt as your environment (i.e., path to the ins and gen folders)
• Go to the top folder, modify the file mag_run.sh (i.e., the path to SystemC library, the GNU Scientific Libarary, the path to MAG)
• In the top folder, modify the file aspectc++_run.sh (i.e., the path to SystemC library, the GSL, the AspectC++)
• Go to the folder ins, modify the Makefile (i.e., the path to SystemC library, the GSL)
• In the top folder run the command make
• Launch Plasma Lab-1.3.8 with the SystemC plugin in the “plugins” folder and then open the producer_consumer.plasma file in gen folder. Please refer to the tutorial of Plasma Lab to know how to check the properties.

Note that you need to install GSL 1.6 or later at /usr/local/lib to compile the examples.