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.
ERCIM FMICS Home Page,
GMD FOKUS Home Page
Last modified: Wednesday, 19-Apr-2000 08:57:51 MET DST,
Axel Rennoch