Formal verification in a component-based reuse methodology

There is an important trend towards design processes based on the reuse of predesigned components. We propose a formal verification approach which smoothly integrates with a component based system-level design methodology. Once a timed Petri net model corresponding to the interface logic has been produced the correctness of the system can be formally verified. The verification is based on the interface properties of the connected components and on abstract models of their functionality, without assuming any knowledge regarding their implementation. We have both developed the theoretical framework underlying the methodology and implemented an experimental environment using model checking techniques.