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

Displayed
Oct 21, 2017
Services in

Introduction

The 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 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 ?

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

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"/>
    <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">

  <leafAttribute name="title" refType="Graph"/>

  <nodeType name="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 checks whether the model conforms to the formalism.

The graph pictured below is followed by its GrML representation.

image/svg+xml u v w
<?xml version="1.0" encoding="UTF-8"?>
<model formalismUrl="http://formalisms.cosyverif.org/graph.fml" xmlns="http://cosyverif.org/ns/model">

  <attribute name="title"> A simple example </attribute>

  <node id="1" nodeType="vertex">
    <attribute name="name">u </attribute>
    <attribute name="initialVertex"> true </attribute>
  </node>
  <node id="2" nodeType="vertex">
    <attribute name="name">v </attribute>
  </node>
  <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 Coloane, the user may invoke the related services (see figure below).

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

Once the service has finished, the results can be seen in the Results View (see figure below).