Affordable Access

Publisher Website

Towards Component Verification in the Generic Component Framework

Authors
Journal
Electronic Notes in Theoretical Computer Science
1571-0661
Publisher
Elsevier
Publication Date
Volume
203
Issue
7
Identifiers
DOI: 10.1016/j.entcs.2009.03.025
Keywords
  • Component Architectures
  • Component Verification
  • Petri Nets
  • Temporal Logic
Disciplines
  • Linguistics

Abstract

Abstract 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.

There are no comments yet on this publication. Be the first to share your thoughts.