Installation

See the downloads page for information about installation.

VECA DSL

For people at ease with grammars, the XText grammar of the VECA DSL is available here.

Signatures

A signature is given as a set of messages (possibly empty), a set of provided operations (possibly empty), and a set of required operations (possibly empty). For operations, the input and the output message are given. It is possible not to have an output message but the input message is mandatory.


  signature
    messages m1, m2, m3;
    provides op1(m1), op2(m1): m2;
    requires op3(m3): m2;

Behaviors

A behavior is given as a transition system with an initial state, final states (at least one), and transition sets. A transition set is given as a source state, and couples made up of an action and a target state. An action can be either an internal action (tau) or a communication action (reception of an operation call, reply to this call, invocation of an operation call, getting the result of this call). 


  behavior
    start in begin;
    stop in end1 end2;
    begin:            receive op1 then end1,
                      receive op2 then compute_arg;
    compute_arg:      tau then call_subservice;
    call_subservice:  invoke op3 then wait_result;
    wait_result:      result op3 then send_reply;
    send_reply:       reply op2 then end2;
    end1:;
    end2:;

Time constraints

A time constraint specifies the minimum and maximum amount of time passing between two communication actions. Time constraints can be used to specify, e.g., the maximum amount of time expected for a required operation (between its invocation and the result), the range in which an operation can be achieved by the component (between the reception and the reply to this operation), or information about the time required to perform an internal operation. Time constraints refer to units of time (uot) and the designer can chose any uniform (for all the model) interpretation for them (1 second, 1 minute, 1 hour, ...). 


  constraints
    invoke op3  -> result op3 : 0 .. 10 // subservice should take at most 10 uot
    receive op2 -> reply op2  : 2 .. 12 // the component takes between 2 and 12 uot to do op2
    receive op2 -> invoke op3 : 1 .. 3; // the internal computation takes between 1 and 3 uot

This component definition is indeed inconsistent, we will see this later on in the verification part.

In this example one may also see that comments are entered using //.

Basic component types

A basic component is given as a signature, a behavior, and (optionally) a set of time constraints.

basic component type Type1 is
  signature ...
  behavior ...
  constraints ...
end

Composite component types

Composite components are made up of sub-components and bindings. Bindings denote binary, possibly two-way, communication channels. There are two kinds of bindings. An internal binding is used for communication between two sub-components of a composite. An external binding is used for communication between the environment of a composite and one of the sub-components of this composite. Using our hierarchical component model, internal, and external bindings, it is possible to have components in different hierarchical level that communicate.

Aspects and weaving

To appear.

All in one

The complete example is as follows.


      to appear

Syntactic verification

The Eclipse VECA plugin (see downloads) provides you with some model verifications that can be performed directly on the VECA model:

Semantic verification

To appear.