CUI LSV LIPN LIP6
MeFoSyLoMa CNRS Iniria
QR Code
Last modified
June 28, 2016

Displayed
Oct 21, 2017
Cosmos in CosyVerif

Introduction

This page is a tutorial on how to use to tool Cosmos in the platform . This tutorial was part of ETR13. The pdf document that was distributed to the students is available there

The main page of the tool can be found here.

The Services Menu

ProdInCosyVerif services are available under the "Behavioral Verification" menu and proposes the elements presented in the image below (number in names are not significative, they just set up a "logical" order in the menu).

the menu

The following services are available:

The Services

Let us know detail the services.

Generate Trajectories of the Model

The first simple analysis we can perform on the tandem queues system is to simulate one trajectory. To do this, select one alligator server in the service menu and then select Cosmos, Generate one trajectory of the model (see figure 5).

A window will pop asking for some parameters. The first page of parameters contains only the length of the trajectory, the second page requires to set the model, check the box of the tandem queue model (see figure 6).

Model
selection box

Once Cosmos finishes the simulation a graphics showing the number of tokens in each place is displayed.

Statistical Performance Evaluation

A more detailed analysis can be performed by choosing the service Cosmos Statistical Perfomance Evaluation in the service menu. This service requires more parameters. You can first keep the default values and launch the service on the tandem queues system. After some time, the result will be displayed. For each place, the tool returns an estimation of the mean number of tokens looking like:

MeanToken_Queue1:	
Estimated value:0.286221703319812	
Confidence interval:[0.282671106477023 , 0.289772300162601]	
Width:0.00710119368557882

For each transition, an estimation of the throughput is returned:

Throughput_rho0:	
Estimated value:0.0999094999999996	
Confidence interval:[0.0985010508695943 , 0.101317949130405]	
Width:0.00281689826081077

You can modify the model by changing the rate rho0 to a value above 0.45 and observe that the system is unstable (meaning the number of tokens in a place diverges) by simulating a trajectory or computing mean number of tokens. You can also try to change the distribution of the first transition from EXPONENTIAL(rho0) to DETERMINISTIC(10) and observe the change on the trace of the simulation. You can try other distributions, the available distributions are (GAMMA, UNIFORM, EXPONENTIAL, DETERMINISTIC, LOGNORMAL, TRIANGLE, GEOMETRIC, DISCRETEUNIF and ERLANG).

Statistical Model Checking over an Automaton

To compute more complex indexes, we will use an automaton to describe them. The LHA model represents an automaton which waits for the system to reach either a state where the total number of clients in the system is equal to 0 or a state where it equals N. In the latter case, the variable x is set to 1. Finally, the expression AVG(last(x)) makes the tool returns an estimation of the expected value of x in final states.

Launch Cosmos statistical model checker service from the service menu. This service requires an LHA, a model and several parameters which can be kept at there default values. The returned result is a confidence interval of an estimation of the expected value of x. A graph depicting the convergence of the estimation is also returned.

You can try to modify parameters of the LHA or of the Model to see the impact on the variable x. You can also try to change the calling parameters of the service to obtain tighter confidence intervals.

You can model a network of queues. Create a new empty model in the Cosmos formalism and build the model depicted in figure 7.

You need to name all places and transitions for the tool to accept the model.

An example of network of waiting queues

You may now adapt the LHA of the previous example to work with this one, computing the probability for the system to reach a state containing N clients before reaching a state with no client.

You can also build an LHA computing the average time between the first arrival of a client and the first time the system is empty. The notation for the flow of a variable is x'=c, where x is the variable and c an expression depending only of the number of tokens is some place. Assuming the variable accounting for the time is t, by replacing the HASL formula by AVG(last(t)); CDF(last(t),0.1,0.0,50.0);, the Cumulative Density Function of the random variable t is returned with the result (see figure 8).

An
example of a computation of CDF

Statistical Model Checking over a Formula

No documentation yet since this service is still under development.