Specification and Verification of the Model of Component and the Model of Function

Due to increasing complexity and competitiveness, automated production systems make, nowadays, higher demands on powerful techniques used to guarantee the requirements of performance and safety. Modeling production systems according to their operating modes allows obtaining a simplified view of these systems. The main difficulty is thus to insure mode changing while guaranteeing the system compatibility and coherence. The solution to this problem relate to modeling methods as well as verification tools. In this paper, we extend our modeling approach of mode handling by introducing adequate verification methods so that the design process will be carried correctly. The Model of Component (MoC) and the Model of Function (MoF) are the basic models of our modeling approach. Thus, we formalize some properties of the MoC and the MoF and we present the corresponding verification methods. We illustrate these methods through an application example. A computer aided tool for specification and verification is developed to illustrate our approach.