The Use of Model Transformation in the INESS Project - Formal Methods for Components and Objects - page 167

1. the local (as opposed to global and temporal) reasoning that is required by
the designer in order to specify behaviour,
2. adaptability to variations in design intent, and
3. checking whether a specification captures the corresponding design intent.

The case study they selected, deals with a switch that internally routes packets
from input buffers to output buffers. These packets are routed according to a set
of rules that specify priority amongst selected packets as well as simultaneous
packet transfers. As these rules are complementary to each other, they illus-
trate contradictive concerns and emphasize on the possible weaknesses of the
specification languages. In [6] it is concluded that each of the used specification
languages performs poorly for at least two of these criteria.
In extension to the framework, presented in [6], this paper puts mCRL2 [9] to
the same test. The goal of this paper is to show that the specification language
mCRL2 is better suited than the other specification languages, at least for the
presented case study.
mCRL2 is a specification language, especially targeted for describing com-
munication behaviour among systems. The behavioural part of the language is
based on process algebra [1]. For the purpose of specifying behaviour, mCRL2
facilitates a data part which is based on higher-order abstract equational data
types. It allows quantifiers, (unbounded) integers, (infinite) sets and bags, struc-
tured types, lists and real numbers, that are set up as close as possible to their
mathematical counterparts.
Themodelsthatwepresentforthecasesare obtained in a relatively straight-
forward way from the informal description. It turns out that multi-party com-
munication is easily captured by the advanced communication mechanisms of
mCRL2. mCRL2 has no direct support for specifying priority. Nevertheless we
are able to describe the types of priority used in the cases at hand.
For the manipulation, analysis and visualisation of specifications, the language
is equipped by a range of tools [7,10]. These tools allow amongst others the
verification of requirements that are described in the modal μ -calculus [13].
This paper is structured as follows. Section 2 gives a brief introduction to
the relevant fragments of the language mCRL2 and the modal μ -calculus. The
switches are modelled in Sections 3,4 and 5. Section 6 elaborates on the require-
ments that have been verified on the constructed models. Section 7 compares
the work presented here to that of others. Section 8 describes our conclusions
and future work.

2 Preliminaries

2.1 Syntax and Semantics of mCRL2

An mCRL2 process is built from data-parameterized multi-actions and a collec-
tion of process operators. In this paper, a fragment of the syntax of the un-timed
mCRL2 language is used. It is given by the following BNF :