|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
| Organisation: |
ISIMA/LIMOS, Université de Clermont-Ferrand (FRANCE)
|
|---|---|
| Method: |
LOTOS and E-LOTOS
|
| Tools used: |
CADP (Construction and Analysis of Distributed Processes) COSMOS |
| Domain: |
Hardware Design.
|
| Period: |
1998-1999.
|
| Size: |
about 300 lines of LOTOS
|
| Description: |
The design of complex systems requires both software and hardware
components, some of them being specifically designed for the
application and others being reused (microprocessors, real-time
kernels, etc.). Codesign methods and tools help the designers
of such systems, by allowing to formally specify and analyse the
system at a high-level of abstraction before synthesizing and
simulating a virtual prototype.
This study presents an approach for linking design and verification environments in the context of hardware/software codesign. The approach is based on refinement steps of the system implementation and ensures automatically the correctness of the refinements. Concretely, the authors have connected the codesign environment COSMOS and the verification environment CADP by providing transformations from the SOLAR models used for codesign and the (E-)LOTOS specifications used for verification. The codesign approach proposed is illustrated on a system containing two producers and one consumer which manages the communication ratios of the producers. The system has been first specified in SDL and the corresponding SOLAR model has been generated using the COSMOS tool. This SOLAR model has been refined by implementing the communication between the producers and the consumer using a single FIFO queue. The refined SOLAR model has been automatically translated in LOTOS and the corresponding labelled transition system has been generated and minimized using CAESAR and ALDEBARAN. This allowed to find automatically a deadlock that resulted from the refinement of the intermediate SOLAR model. |
| Conclusions: |
The specification and model-based analysis features provided by
toolsets such as CADP proved to be useful in the domain of
hardware/software codesign. The integration of toolsets from both
hardware design and formal verification areas is a promising way
towards a complete environment for building complex hardware/software
systems.
|
| Publications: |
[Wodey-Baray-99]
P. Wodey and F. Baray.
"Linking Codesign and Verification by means of E-LOTOS FDT".
Proceedings of the Euromicro Workshop on Digital System
Design: Architectures, Methods and Tools (Milan, Italy),
September 1999.
Available online from the CADP Web site in PDF 
or
PostScript 
[Baray-Wodey-00] F. Baray and P. Wodey. "Verification in the Codesign Process by means of LOTOS Based Model-Checking". In S. Gnesi, I. Schieferdecker, and A. Rennoch, editors, Proceedings of the 5th International Workshop on Formal Methods for Industrial Critical Systems FMICS'2000 (Berlin, Germany), GMD Report 91, pp. 87-108, Berlin, April 2000. Available online at: http://www.fokus.gmd.de/research/cc/tip/fmics/abstracts/baray.html or also from the CADP Web site in PDF
or
PostScript
|
| Contact: | Pierre Wodey ISIMA/LIMOS BP 125 F-63173 Aubière Cedex France Tel: +33 (0)4 73 40 50 12 Fax: +33 (0)4 73 40 50 01 E-mail: Pierre.Wodey@isima.fr |
| Further remarks: | This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies |
Back to the CADP case studies page