Database of Case Studies Achieved Using CADP

Hardware/Software Codesign.

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 our FTP 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 our FTP 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


Last modified: Fri Feb 19 09:12:04 2016.


Back to the CADP case studies page