AUTHORS

G. Huecas, T. Robles

Tlf: +34 1 549 57 00 x 442
Fax: +34 1 336 73 33
DIT-UPM
Technical University of Madrid
Ciudad Universitaria s/n, 
28040 Madrid SPAIN
gabriel@dit.upm.es


L.M. Gonzalez

GMV S.A.
c/Isaac Newton, 11, 28760 Madrid SPAIN
lmgonzalez@gmv.es


J. Serrano

CRISA S.A.
c/Torres Quevedo, 9, 28760 Madrid SPAIN
serrano@crisa.es

ABSTRACT

In December 1996, a project called LVARTS was finished
and delivered to the ESA. The goal was to validate a real
system, namely ATAC, an ADA co-processor chip, running on
a real board. The system was big enough to develop specific
methodologies and tools, which are described in this paper.
LOTOS was chosen to formally specify ATAC. The formal
specification was used to produce test cases that were
executed against the chip, after a completion process to
obtain executable test cases.


This paper is based on the experience gained from the
Project "LOTOS Validation of an ADA Runtime System",
ESA contract No. 10797/94/NL/FM(SC), carried out by CRISA,
GMV and DIT-UPM (hereby, the Consortium) and started in
April 1994 and finished in December 1996.

The objective was to apply rigorous validation strategies on
a Complex Hardware System (the ADA Tasking Co-processor- ATAC)
based on Formal Description Techniques (FDTs). This implies
the definition and developing of theoretical and practical
procedures, concepts, tools and whatever were needed for
validating the real, big, complex system working in a real
environment.

The project was divided in three major phases, as the chip was
available and it was not needed to develop it:

1. Production of the User Requirement Document (URD) of ATAC.

2. Specification of ATAC in LOTOS, including the validation of
the formal specification against the URD.

3. To develop a Validation Environment and to derive Conformance
Test Cases (through a Conformance Test Tool also generated within
the project) from the formal specification.

4. To validate a real ATAC implementation that consisted of a
board using the MA31750 (P and the co-processor ATAC.

This paper focused on point 3, as it was intended by the Consortium
that both the Methodology and the tools were as general as possible,
so it could be applied to other systems, even using other FDTs.