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

Nadia HAMANI
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.

>>Full text
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.

1. Introduction

For the requirements of the Automated Production Systems (APS) control functions, it is necessary to know all operating modes and states of a system and its subsystems and also their changing conditions. However, due to increasing complexity of APS, some problems appear during state or mode changing if safety constraints are not taken into account in the specification/modeling stages.

Dependable modeling methods must be developed to deal with an increasing complexity and safety requirements. Several approaches are proposed in the literature [9][13]. These approaches focus on modeling, without dealing with the verification of the proposed models. However, these models should be verified at the early stages of the design process. A greater interest is allocated in our research team to verification methods, which guarantee that the developing models of APS respects some properties. That is why in this work we extend our modeling approach of mode handling [8][12] by developing formal verification tools so that the design process will be performed correctly.

We proposed in [8] a modeling method of the behavior of production systems from the point of view of their modes. The system is modeled using a Functional Graph (FG) of Exploitation obtained according to an analysis approach based on production goals. We should determine the main goals for which the system was designed and the sub goals that allow to reach them; each one of the sub goals can be decomposed in the same manner until obtaining the initial goals. These are the leaves of the graph; they are related to the resources which perform the initial goals. The behavior of the resources and the functions is specified in order to know constantly their states. For each function or resource, several concurrent families of modes are determined according to a multipoint of view method. The obtained models representing the behavior of the resources and the functions are respectively called Model of Component (MoC) and Model of Function (MoF). They are the basic models of this design approach.

As explained above, adequate verification methods should be developed for our modeling method. In this paper we introduce some properties of the MoC and the MoF and the corresponding verification methods using graph theory.

In the following section we present the main characteristics of our modeling approach for mode handling and the design process of the APS behavioral model. We extend this process by integrating appropriate verification methods. Section 3 presents some properties of the MoC and the MoF and the corresponding verification methods. In section 4, we illustrate our propositions through an application example. Finally, in section 5, we discuss some future prospects.

REFERENCES:

ADEPA, Le GEMMA, Guide d’Etude des Modes de Marches et d’Arrêts, Production Automatisée, ADEPA, 1981.
ALJ, A. and FAURE R., Eléments de la théorie des graphes, Guide de la recherche opérationnelle, T.1. Les fondements, MASSON (France), 1986. Ch. 2.
ARNOLD, A., GUESSARIA I., Mathématiques pour l’informatique, MASSON (France), 1993.
AUSFELDER, C., MAIK J.P., KERMAD L., GENTINA J.C., DELFIEU D., MOISAND R. and SAHRAOUI A.E.K., Integration of operating modes in the control of flexible manufacturing systems combining synchronous and asynchronous approaches, Proc. of IEEE Int. conf. on Systems Man and Cybernetics (SMC 93), Le Touquet, France, 1993.
BILAND, P., Modélisation des Modes de Marche d’un Système Automatisé de Production, Ph.D. dissertation, Ecole de Centrale de Nantes, Nantes, France, 1994.
BILAND, P., DEPLANCHE A.M. and ELLOY J.P., A Model for Operating Modes of Computer Integrated Manufacturing Systems, Proc. of the European Workshop on Integrated Manufacturing Systems Engineering (IMSE 94), Grenoble, France, 1994.
BOIS, S., CRAYE E. and GENTINA J.C., Manager of Working Modes, CIM Integ. Design. in Manufacturing 21(3), 1992.
DANGOUMAU, N., Contribution à la Gestion des Modes des Systèmes Automatisés de Production, Ph.D. dissertation, Université des Sciences et Technologies de Lille, Lille, France, 2000.
DANGOUMAU, N., DUMERY J.J., FAURE J.M. and CRAYE E., Prise en compte des modes de marche dans le pilotage, in Fondements du pilotage des systèmes de production, HERMES (France), IC2, 2002, Ch. 5, pp. 155-180.
DANGOUAMAU, N., Utilisation du Graphe Fonctionnel pour la gestion des modes d’un SAP, presented at the DES research team seminar, LAGIS, juin 2003.
GONDRAN, M. and MINOUX M., Graphes et Algorithmes, Collection de la Direction des Etudes et Recherches d’Electricité de France, EYROLLES (France), 1995.
HAMANI, N., DANGOUMAU N. and CRAYE E., Design Analysis and Verification of the Model of Component, Proc. of the 10th Int. Multi-Conf. on Advanced Computer Systems (ACS 03), Miedzyzdroje, Poland, 2003.
HAMANI, N., DANGOUMAU N. and CRAYE E., A Comparative Study of Mode Handling Approaches, Proc. of the 35th Int. Conf. on Computers & Industrial Engineering (CIE 05), Istanbul, Turkey, 2005.
HAMANI, N., DANGOUMAU N. and CRAYE E., A Computer Aided Tool for Specification and Verification of the MoC and the MoF, Proc. of the Int. Joint Conferences on Computer, Information – International Conference on Industrial Electronics, Technology & Automation, and Systems Sciences, and Engineering (CISSE-IETA’06), USA, 2006.
KERMAD, L., CRAYE E., BOUREY J.P. and GENTINA J.C., The Exploitation Modes of Flexible Manufacturing Systems, Proc. of IEEE Int. Conf. on Systems Man and Cybernetics (SMC 94), San Francisco, USA, 1994.
PARAYRE, T., SALLEZ Y. and SOENEN R., Model of the State of Operation of Automated Systems, Proc. of the 8th Int. PROLAMAT conference (PROLAMAT 92), Tokyo, Japan, 1992.
TOGUYENI, A.K.A., ELKHATTABI S. and CRAYE E., Functional and/or Structural Approach for the Supervision of Flexible Manufacturing Systems, Proc. of IMACS-IEEE Multi-Conf. on Computational Engineering in Systems Applications (CESA 96), Lille, France, 1996.
TOGUYENI, A.K.A., Contribution à la tolérance aux fautes des Systèmes Flexibles de Production Manufacturière, H.D.R. dissertation, Université des Sciences et Technologies de Lille, Lille, France, 2001.