Towards Component Verification in the Generic Component Framework

The intention of this paper is to extend the generic component framework presented at FASE 2002 [H. Ehrig, F. Orejas, B. Braatz, M. Klein, and M. Piirainen. A Generic Component Concept for System Modeling. In Proc. FASE 2002: Formal Aspects of Software Engineering, volume 2306 of Lecture Notes in Computer Science, pages 32–48. Springer Verlag, 2002] to allow component verification based on export-import implications. In the generic component framework components with explicit import, export interfaces and a body specification connected by embeddings and transformations provide hierarchical composition of components with a compositional transformation semantics.We introduce implications that relate sentences of the import stating what the component requires to sentences of the export stating what the component guarantees. The main result of this paper is that these import-export implications are compatible with the hierarchical composition as given in [H. Ehrig, F. Orejas, B. Braatz, M. Klein, and M. Piirainen. A Generic Component Concept for System Modeling. In Proc. FASE 2002: Formal Aspects of Software Engineering, volume 2306 of Lecture Notes in Computer Science, pages 32–48. Springer Verlag, 2002]. The second part illustrates how this abstract concept can be instantiated to Petri net systems