INRIA Rhône-Alpes / VASY (FRANCE)
FMT group / University of Twente (THE NETHERLANDS)
CADP (Construction and Analysis of Distributed Processes)
about 150 lines of LOTOS
When designing complex systems, it is desirable to address
functional correctness and performance evaluation within the same
framework, for both scientific and economic reasons. A successful
approach to achieve this relies on existing description languages
such as the ISO standard LOTOS and state-of-the-art verification
tool sets such as CADP. Basically, the approach consists in starting
from a functionally verified LOTOS specification, in which timing
information is introduced to express that certain events are delayed
by a random time. To support this methodology, the components of
CADP are used together with a novel tool named BCG_MIN, which allows
to minimize stochastic models. The approach is illustrated by an
industrial case-study: the bus arbitration protocol used in the
SCSI-2 (Small Computer System Interface) standard.
The system considered consists of at most 8 devices (7 hard disks and a disk controller) connected by a bus implementing the SCSI-2 standard. Each device is assigned a unique SCSI number between 0 and 7. Engineers at Bull discovered in the early 90's potential starvation problems for disks having SCSI numbers smaller than the SCSI number of the disk controller. The problem was first investigated by Massimo Zendri, who developed a Markovian queing model to study performance issues. Later, the functional aspects of the SCSI-2 arbitration protocol were formalised in LOTOS by Hubert Garavel, with an emphasis on modelling arbitration concisely using LOTOS multiway rendezvous. This LOTOS specification served as a basis for model-checking by Radu Mateescu, allowing to rediscover the starvation problem mechanically. The same LOTOS specification is also used as basis for studying performance issues in the present work.
In the SCSI-2 system, the controller can send randomly to the disk n a message "CMD !n" (command) indicating a transfer request (read/write a block of data from/to the disk). After processing this command, the disk sends back to the controller a message "REC !n" (reconnect). The CMD and REC messages are stored in 8-place FIFO queues; since the contents of these messages are not modelled, the queues are represented as simple counters in the LOTOS specification. The CMD and REC messages circulate on the SCSI bus, which is shared by all devices. To avoid access conflicts, the SCSI-2 standard defines a bus arbitration protocol based on fixed priorities: if several devices want to access the bus simultaneously, the device with the highest SCSI number is granted access. The devices are modelled as LOTOS processes executing concurrently. The arbitration (inspection of the bus content by all devices) is modelled by a multiway LOTOS rendezvous with value negotiation and pattern-matching.
To study performance aspects, the LOTOS specification is enhanced with additional information about timing characteristics:
A practical methodology was presented for studying the performance
of a concurrent system starting from an already verified functional
specification of this system. The approach is original in several
respects: (a) it does not define a new formalism for modelling
stochastic systems, but relies on the existing LOTOS formal
description technique, adapted to the stochastic framework by adding
timing information; (b) the CADP tools are used for constructing the
LTS of the LOTOS specifications, and BCG_MIN is used to minimize
these LTSs in the stochastic setting; (c) automation of the performance
experiments is achieved by means of the SVL scripting language,
which allows to integrate various tools transparently.
[Garavel-Hermanns-02] Hubert Garavel and Holger Hermanns.
"On Combining Functional Verification and Performance Evaluation
using CADP". In Lars-Henrik Ericsson and Peter A. Lindsay, editors,
Proceedings of the 11th International Symposium of Formal Methods
Europe FME'2002 (Copenhagen, Denmark), Lecture Notes in Computer
Science vol. 2391, pp. 410-429. Springer Verlag, July 2002. Full
version available as INRIA Research Report 4492.
Available on-line at: http://cadp.inria.fr/publications/Garavel-Hermanns-02.html
INRIA Rhône-Alpes / VASY
655, avenue de l'Europe
F-38330 Montbonnot Saint Martin
Tel: +33 (0)4 76 61 52 24
Fax: +33 (0)4 76 61 52 52
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|