The CosyVerif platform offers a set of services that can be operated on models. Each model must respect the definition of a formalism. Then, when you connect to CosyVerif using a client, you may browse and activate the services that are available for this formalism.

The sections below provide more information about services.

What is a formalism of CosyVerif?

A formalism defines a class of labelled oriented graphs. It consists of:

• Defining the different kinds of vertices
• Defining the different kinds of edges
• Associating attributes with vertices
• Associating attributes with edges
• Defining global attributes

The formalism is described in a dialect of XML called FML.

Here is an example of an unlabelled oriented graph with a single kind of vertex and edge.

<?xml version="1.0" encoding="UTF-8"?>
<formalism name="Graph" xmlns="http://cosyverif.org/ns/formalism">
 
  <nodeType name="vertex"/>
 
  <arcType name="transition"/>
 
</formalism>

Suppose that we want to check reachability. First we give names to vertices, then we add an attribute to the vertices denoting the initial vertices.

By default, this attribute is false.

<?xml version="1.0" encoding="UTF-8"?>
<formalism name="Graph" xmlns="http://cosyverif.org/ns/formalism">
 
  <nodeType name="vertex"/>
 
  <!-- attributes of vertex -->
  <leafAttribute name="name" refType="vertex"/>
  <leafAttribute name="initialVertex" refType="vertex" default="false"/>
 
  <arcType name="edge"/>
</formalism>

Finally if the graph has an identifier called title, a global one is defined as follows.

<?xml version="1.0" encoding="UTF-8"?>
<formalism name="Graph" xmlns="http://cosyverif.org/ns/formalism">
 
  <!-- global attribute -->
  <leafAttribute name="title" refType="Graph"/>
 
  <nodeType name="vertex"/>
 
  <!-- attributes of vertex -->
  <leafAttribute name="name" refType="vertex"/>
  <leafAttribute name="initialVertex" refType="vertex"/>
 
  <arcType name="transition"/>
 
</formalism>

How to define a model of a formalism?

A model of a formalism is also described in a dialect of XML called GrML. Once the formalism is defined, a tool integrated in CosyVerif checks whether the model conforms to the formalism.

The graph pictured below is followed by its GrML representation.

<?xml version="1.0" encoding="UTF-8"?>
<model formalismUrl="http://formalisms.cosyverif.org/graph.fml" xmlns="http://cosyverif.org/ns/model">
 
  <!-- title of the model -->
  <attribute name="title">A simple example</attribute>
 
  <!-- vertex u -->
  <node id="1" nodeType="vertex">
    <attribute name="name">u</attribute>
    <attribute name="initialVertex">true</attribute>
  </node>
 
  <!-- vertex v -->
  <node id="2" nodeType="vertex">
    <attribute name="name">v</attribute>
  </node>
 
  <!-- vertex w -->
  <node id="3" nodeType="vertex">
    <attribute name="name">w</attribute>
  </node>
 
  <arc id="101" arcType="edge" source="1" target="2"/>
  <arc id="102" arcType="edge" source="2" target="1"/>
  <arc id="103" arcType="edge" source="2" target="3"/>
 
</model>

More information can be found here.

From models to tools

At any time during model edition by CosyDraw, the user may invoke the related services (see figure below).

Then, after selecting a service (here Imitator), the user is requested to provide the parameters of the invocation (see figure below).

Once the service has finished, the results can be downloaded in the Output section (see figure below).