|Final Report of the COST-247 Action|
Validation of Hardware Implementations using Formal Description Techniques
G. Huecas (1), T. Robles (1), L.M. Gonzalez(2), J. Serrano (3)
|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|
|(2) GMV S.A.|
|c/Isaac Newton, 11, 28760 Madrid SPAIN|
|(3) CRISA S.A.|
|c/Torres Quevedo, 9, 28760 Madrid SPAIN|
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:
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.