Laboratoire Universitaire de Recherche en Production Automatisée (LURPA)
avenue du Président Wilson, 94235 Cachan cedex, France
Nathalie DANGOUMAU, Etienne CRAYE
Laboratoire d’Automatique, Génie Informatique et Signal (LAGIS)
Ecole Centrale de Lille, BP.48 59651 Villeneuve d’Ascq cedex, France
Abstract: 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.
Keywords: Automated Production Systems, control system, supervision, mode handling, modeling, graph theory, verification.
CITE THIS PAPER AS:
Nadia HAMANI, Nathalie DANGOUMAU, Etienne CRAYE, Specification and Verification of the Model of Component and the Model of Function, Studies in Informatics and Control, ISSN 1220-1766, vol. 17 (1), pp. 27-42, 2008.