5th International Workshop on

Formal Methods for Industrial Critical Systems

Berlin, April 3-4, 2000

Verification in the Codesign process by means of Lotos based model-checking

This paper presents an approach for linking Design and Verification environments in the context of hardware/software Codesign of complex systems. The considered Codesign tool is based on refinement steps of the system implementation. We describe the advantage in the integration of verification in the refinement process for detecting easily and early design errors consisting in deadlocks in the system. In this study, we consider the Cosmos Codesign environment based on a specific internal representation of the system. The proposed approach consists in translating this internal representation into a verification dedicated representation. This translation is formally presented with inference rules and can be applied to many finite state communicating machines models. A model-checking technique, with Cadp verification toolbox and the Lotos language as verification dedicated representation of the system, is used to find the system errors efficiently. In order to detect global or local deadlocks, some temporal formulas are generated in Xtl language, and verified on the system with the Xtl model-checker included in the Cadp toolbox.

Note: The content of the following files is part of GMD Report No. 91 and subject to its copyright.


Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST, Axel Rennoch