Getting Started

Downloading and installing the ePMC tool

The ePMC Tool is provided a zip file containing Java programs, bash script files and a number of supporting files. Start by downloading the zip file from this location. Then extract the zip file to a folder on your local machine, making a note of the directory location to which the tool is extracted.

Please note that the current version of ePMC has been tested on MacOX 10.14 and Ubuntu 16.4.

Additional Software

ePMC makes use of third party model checkers and you will need to install these on your machine before running ePMC. You may use either PRISM which is available from https://www.prismmodelchecker.org or Storm available from http://www.stormchecker.org. Having installed the model checker of your choice make a note of the installation location as you will need to configure ePMC to find the tool.

Configuring ePMC

In the directory where you extracted the ePMC tool there will be two text files: Open the file which corresponds to your model checker of choice and edit the location in the file to match the location on your local machine.

Next open the file ePMC-Prism.sh in a text editor and find the line

toolLoc="/local/sda7/cap508/ePMC2"

Edit this line such that the directory matches the location where you extracted the ePMC tool. Repeat for the ePMC-Storm.sh file.

Annotating a model for ePMC

The ePMC model checker supports the analysis of pattern-annotated parametric Markov chains specified in the high-level modelling language used by PRISM and Storm. This language models a system as the parallel composition of a set of modules. The state of a module is encoded by a set of finite-range local variables, and its state transitions are defined by probabilistic guarded commands that change these variables, and have the general form:

[action] guard -> e1: update1 + . . . + eN : updateN ;

In this command, guard is a boolean expression over all model variables. If guard evaluates to true, the arithmetic expression ei, 1 ≤ i ≤ N, gives the probability with which the updatei change of the module variables occurs. When the label action is present, all modules comprising commands with this action have to synchronise (i.e., can only carry out one of these commands simultaneously).

In the header of the model we add pattern annotations of the form:

/// id : pattern_name(actual_parameter_list)

where the triple-slash notation, '///' indicates a comment for the model checker and a command for ePMC. For example the following annotations define modelling patterns for three components. 'The first two are both "sequential with probabilistic retry" (SEQ_R1) with two services and the third is a "probabilistic" pattern with 3 services.

/// 1:SEQ-R1(p11,c11,t11,p12,c12,t12,r1)
/// 2:SEQ-R1(p21,c21,t21,p22,c22,t22,r2)
/// 3:PROB(p31,c31,t31,p32,c32,t32,p33,c33,t33,x31,x32,x33)

Next we define variables in the model that are associated with each of the components and their QoS properties by using the component ID within the variable. For example with reference to component id:1 we would define:

const double prob1;
const double cost1;
const double time1;

Next, we use these variables in the model, e.g. within rewards structures:

rewards "time"
 z=1: time1;
 z=2: time2;
 z=3: time3;
endrewards

Finally, we may require models parameters NOT associated with the internal operation of system components to also be present in the Matlab file generated. In such cases we can annotate the variable using the triple slash notation as folllows:

const double x; /// ePMC-Var
const double y; /// ePMC-Var

Running ePMC

ePMC is run from a terminal window as follows:

ePMC-Storm.sh model.pm properties.pctl output.m

or

ePMC-Prism.sh model.pm properties.pctl output.m