ISIMA/LIMOS, Université de Clermont-Ferrand (FRANCE)
LOTOS and E-LOTOS
CADP (Construction and Analysis of Distributed Processes)
about 300 lines of LOTOS
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.
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
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),
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
F-63173 Aubière Cedex
Tel: +33 (0)4 73 40 50 12
Fax: +33 (0)4 73 40 50 01
|Further remarks:||This case study, amongst others, is described on the CADP Web site: http://cadp.inria.fr/case-studies|