Linking codesign and verification by mean of E-LOTOS FDT

摘要

This paper presents an approach for linking design and verification environments in the context of hardware/software codesign of complex systems, 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. Generally, design tools are based on a specific internal representation of the system, and classical approach for linking design and verification consists in translating this representation into a verification dedicated representation. The originality of the proposed approach in this paper consists in applying in parallel the refinement transformations on two specific representations of the system: one dedicated to the implementation and synthesis and the other dedicated to verification. A simple example shows the advantages of using such an approach when considering model checking verification techniques: the size of the model is significantly decreased. In this study, we consider the COSMOS Codesign environment, the OPEN/CAESAR verification toolbox and the E-LOTOS language as verification dedicated representation of the system.