|
|
|
|
Dyade is a joint venture between Bull and Inria for advanced research. Within Dyade, the Vasy action targets at the application of formal methods and tools developed at INRIA to the design of several multiprocessor architectures developed at Bull.
The Vasy project emcompass several working areas:
The formal specification task consists in producing a mathematical, unambiguous model of the complex architecture/protocol under study. The modeling is done at an abstract level that hides the irrelevant implementation details. The specification language used is LOTOS (ISO standard 8807). Formal specification often allows to clarify ambiguities and to detect design errors at the very beginning of the development process.
The formal specification can be used as a basis to generate executable code using a LOTOS compiler. The generated code serves for simulation and emulation purpose. This allows to perform further debugging of the design, taking advantage of the available formal specification. The toolset used for compiling LOTOS programs is CADP (Caesar/Aldebaran Development Package).
Simulation and emulation allow some debugging of the formal specification, but do not give a total confidence in the correctness of the design. Using model-checking techniques, it is possible to verify critical requirements on down-sized configurations exhaustively, while the traditional tests and simulations are used to perform non-exhaustive verification on larger configurations. The toolset used for verification is CADP.
It consists in generating test cases from a formal specification and formal test purposes. This approach cuts the costs of test activity: the automatically generated test cases send inputs to the implementation and check that the implementation's outputs are correct with respect to the formal specification. This avoids the manual writing of all the interactions of a test case and the development of a test checker; by doing so, more complex tests and a better test coverage can be obtained. The test generation tool used is TGV (Test Generation using Verification technology).
The benefits of the approach used in the Vasy project are the following:
Although there is an extra cost during the design phase (due to formal specification and verification), this cost is considered as a quality insurance cost.
Starting date: January 1995 (officially created in 1996)
Ending date: 1998
Client within Bull: Bull R&D site in Pregnana (Italy)
INRIA hosting projects: Vasy-RA (INRIA Rhône-Alpes), Pampa (INRIA Rennes)
Operational supervision: Nadia Tawbi [1995], Ghassan Chehaibar [1996-1997], Massimo Zendri [1997-1998] (Bull)
Scientific supervision: Hubert Garavel (INRIA Rhône-Alpes) and Claude Jard (INRIA Rennes)
| Team Members: |
Ghassan Chehaibar (Bull) Christophe Discours (INRIA Rhône-Alpes) Hubert Garavel (INRIA Rhône-Alpes) Claude Jard (INRIA Rennes) Thierry Jéron (INRIA Rennes) Mark Jorgensen (INRIA Rhône-Alpes) Hakim Kahlouche (INRIA Rennes) Radu Mateescu (INRIA Rhône-Alpes) Pierre Morel (INRIA Rennes) Laurent Mounier (INRIA Rhône-Alpes/Verimag) Laurence Nedelka (INRIA Rennes) Mihaela Sighireanu (INRIA Rhône-Alpes) Nadia Tawbi (Bull) César Viho (INRIA Rennes) Massimo Zendri (Bull) |
In 1995, the project started with a preliminary case-study, in order to assess both the feasibility of applying formal methods to hardware design and the proper functioning of the LOTOS tools developed at INRIA Rhône-Alpes. For this purpose, Bull selected an already existing protocol, the bus arbiter protocol of the PowerScale architecture used in Bull's Escala series of Unix workstations.
The PowerScale bus arbitration protocol was specified formally (720 lines of LOTOS). Four correctness requirements were identified for this protocol (concerning deadlock freeness, fairness of arbitration, ordering of grants with respect to requests, and flow control). These requirements were verified using compositional model-checking, thus indicating the correctness of the protocol (this was not surprising as the PowerScale architecture had already been validated by Bull). It was also demonstrated that some of the correctness requirements would not be satisfied if the protocol was modified to introduce some design mistakes found in earlier versions of the protocol.
This work led to a publication. It was decided to continue the Bull-INRIA collaboration on formal methods, by tackling a new case study.
From 1996 to July 1998, the Dyade/Vasy team worked on Polykid, a prototype CC-NUMA multiprocessor architecture developed at the Bull R&D center located in Pregnana, near Milano (Italy). The study focused on the cache coherency protocol, which was the most complex protocol of Polykid.
Contrary to the PowerScale case-study in which formal methods were applied to an already existing product, the Polykid case-study was different, in the sense that formal methods were fully integrated within the industrial development process. In particular, the formal specification activity took place in parallel with the development of the Polykid architecture in Pregnana, which required a close relationship with the architects from the earlier phases of the project.
The work done during the Polykid project followed three main scientific axes:
Several LOTOS specifications of the Polykid cache coherency protocol (between 2,000 and 4,000 lines of LOTOS) were elaborated, corresponding to the successive revisions of the informal specifications of the Polykid architecture.
This modeling activity raised 85 questions sent to the Polykid architects. Many of these questions were merely requests for clarification of the informal specification. However, 20 questions unveiled major issues in the design of the cache coherency protocol: in particular, 9 of these 20 issues were actual behavioural errors (such as deadlock or data coherence loss), while the other issues were about ambiguities and incomplete specifications (undocumented cases).
The LOTOS descriptions were simulated and verified (using abstractions and compositional verification) using the CADP tools. For some errors, the verification tools were used to check that the corrections proposed by the architects solved the problems at the same simplified and abstracted level than the model.
Thus, the formal specification and verification of a down-sized configuration of the protocol allowed to clarify design issues and detect problems: some would have been difficult to detect and understand through traditional tests and simulations. This activity was considered very profitable by the architecture designers.
Another aspect of the Polykid experiment is related to the problem of hardware-software codesign and, more specifically, to the software emulation of hardware circuits. At the time of the case-study, an essential component of the Polykid architecture, the RCC (Remote Cache Controller) was not available, thus preventing Bull from testing the Polykid architecture in whole.
To overcome this problem, a LOTOS specification of the RCC behaviour was produced (3,300 lines of LOTOS). This formal specification activity revealed several ambiguities, as well as 3 design errors (including potential deadlocks) in the informal specifications of the RCC.
Then, this LOTOS description was automatically translated into C code using the LOTOS compilers Caesar and Caesar.adt available within the CADP tool set. The interface between the LOTOS specification and the environment was handled by an extension of Caesar called Exec/Caesar. The generated C code was then compiled to PowerPC object code and embedded on a PowerPC motherboard inserted in a Polykid machine to emulate the missing RCC circuit. The goal of this experiment was to emulate the chip for anticipating the development and testing of firmware/software for the Polykid machine.
As such, the software emulation was found to be working, yet not fast enough to reach the required speed of the RCC hardware circuit (100,000 transactions per second). For this reason, it was decided to rewrite partly in C the LOTOS specification of the RCC (the behaviour part was rewritten in C, while the C code generated from the data part was kept unchanged): this enabled to reach the desired level of performance. In parallel, work took place to increase (by a factor ranging from 10 to 150) the speed of the C code generated by the Caesar compiler for the behaviour part.
This work on software emulation of hardware circuits received a Bull R&D Award granted by an independent jury in 1997.
The test generation tool TGV was applied to the LOTOS descriptions of Polykid in order to generate test cases defined by test purposes. This approach allowed to generate automatically about 200 simple tests, which cover entirely the test suite planned for Polykid (except the random tests and configuration tests, which can be generated using an already existing Bull methodology).
Then, the TGV tool was enhanced to generate so-called "generalized tests" (each generalized test corresponding to several hundreds, or even several thousands, of simple tests). For Polykid, about 10 generalized tests have been generated, which even increased the coverage of the test plan.
A connection was established between the tests generated by TGV and the VSS (VHDL Synopsis Simulator) tool used by the Polykid developers. This connection allowed to pass the tests generated by TGV on the Polykid implementation. This revealed 5 serious inconsistencies (regarding the cache updates) between the LOTOS description and the VHDL implementation of the RCC circuit (version 2).
The Polykid experiment demonstrated that the automatic test generation approach is a true alternative to the traditional approach based on hand-written tests. Moreover, all the tests generated automatically are correct with respect to the LOTOS specification, which avoids the problem of potential errors in hand-written tests.
This work led to several publications. Also, it is worth noticing that, during the Polykid experiment, the CADP and TGV tools have been notably enhanced. Even if Bull did not made of Polykid a commercial product, the use of formal methods in the Polykid development was considered to be profitable. Upon termination of the Dyade/Vasy action in September 1998, it was decided to continue the Bull-INRIA collaboration on formal methods by initiating a new co-operative project, the FormalFame action.
[1]
Specification and Verification of the PowerScale Bus
Arbitration Protocol : An Industrial Experiment with LOTOS
Ghassan Chehaibar and Hubert Garavel, Laurent Mounier, Nadia Tawbi,
Ferruccio Zulian
Proceedings of the Joint International Conference on Formal
Description Techniques for Distributed Systems and Communication
Protocols, Protocol Specification, Testing and Verification,
FORTE/PSTV'96 (Kaiserslautern, Germany),
1996, Ed. Reinhard Gotzhein and Jan Bredereke, pp 435--450,
IFIP, October, Full version available as
INRIA Research Report, RR-2958.
[2]
An Industrial Experiment in Automatic Generation of Executable
Test Suites for a Cache Coherency Protocol
H. Kahlouche, C. Viho, M. Zendri
in Proceedings of IWTCS'98 "International
Workshop on Testing of Communicating Systems", Tomsk, Russia,
September 1998
[3]
Hardware testing using a communication protocol conformance
testing tool
H. Kahlouche, C. Viho, M. Zendri
in Proceedings of the Fifth International Conference on Tools and
Algorithms for the Construction and Analysis of Systems
(TACAS'99), Amsterdam, the Netherlands, March 1999
[4]
System Design of a CC-NUMA Multiprocessor Architecture using Formal
Specification, Model-Checking, Co-Simulation, and Test Generation
H. Garavel, C. Viho, M. Zendri
INRIA Research Report RR-4041, November 2000
Rapport d'activité Dyade/Vasy 1996 (in French)
Rapport d'activité Dyade/Vasy 1997 (in French)
Rapport d'activité Dyade/Vasy 1998 (in French)
See also the yearly activity reports of the INRIA/VASY team, available from the Press Releases Page.
Back to the VASY Home Page