University

This example is studied here. The goal is to model humoristically some communications flows between the administration of a university and its researchers. The system is composed by three components: the Administration, a Researcher and a serving Machine. The normal behavior is that the administration receives grants and produces coins that can be inserted into the serving machine. Then the machine can produce either coffee or tea, that is drunk by the research in order to write publications, which in the end are transformed into patents by the administration. At tutorial of the tool based on this example is presented in the usage section.

Machine	Researcher
Administration	University

The correctness of this system is expressed in a global specification University that specifies that when a grant is received by the university a patent will eventually be produced. We can check this specification in PyECDAR by the following refinement relation:

Machine | Researcher | Administration

It turns out to be false due to the abilities of the serving machine to produce a free and of the administration that can accept a publication before receiving a grant.

Additionally in PyECDAR we can check the consistency, the robust consistency, the compatibility and the robust compatibility of these components and of their parallel compositions. We give below benchmark results for the verification of these properties with PyECDAR. In this test we compare in particular the parametric counter-example approach (CR) for robustness analysis with a binary search approach (BS).