Validation of Hardware Implementations using Formal Description Techniques

Final Report of the COST-247 Action

G. Huecas (1), T. Robles (1), L.M. Gonzalez(2), J. Serrano (3)

(1) DIT-UPM

Technical University of Madrid

Ciudad Universitaria s/n

28040 Madrid SPAIN

Tel : +34 1 549 57 00 x 442

Fax : +34 1 336 73 33

E-mail: gabriel@dit.upm.es

~

(2) GMV S.A.

c/Isaac Newton, 11, 28760 Madrid SPAIN

E-mail: lmgonzalez@gmv.es

~

(3) CRISA S.A.

c/Torres Quevedo, 9, 28760 Madrid SPAIN

E-mail: 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:

Production of the User Requirement Document (URD) of ATAC.
Specification of ATAC in LOTOS, including the validation of the formal specification against the URD.
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.
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.

This presentation has been given during the COST-247 2nd International Workshop on Applied Formal Methods in System Design (Zagreb, Croatia, June 18-19, 1997).

COST-247 Working Group(s):

Web Links :

This Page was prepared by Mark Jorgensen.

Back to the VASY Home page