This paper presents a formal method supporting hardware/software co-design with respect to specification and verification. We introduce three different specification formats. Two of these are intended for the specification of asynchronous software; the third is more suited for digital hardware applications. All three formats are based on the assumption/commitment paradigm. We introduce a refinement relation and formulate verification rules for the parallel composition of specifications. We apply the proposed method to specify and decompose a timed FIFO queue which is partly to be implemented in hardware and partly to be implemented in software.     «

This paper presents a formal method supporting hardware/software co-design with respect to specification and verification. We introduce three different specification formats. Two of these are intended for the specification of asynchronous software; the third is more suited for digital hardware applications. All three formats are based on the assumption/commitment paradigm. We introduce a refinement relation and formulate verification rules for the parallel composition of specifications. We appl...     »