An Iterative Method for the Design Process of Mode Handling Model
Keywords:
Flexible Manufacturing Systems, supervision, mode handling, functional and behavioral modeling, verification, validationAbstract
This paper focuses on formal verification and validation of a model dedicated to mode handling of flexible manufacturing systems. The model is specified using the synchronous formalism Safe State Machines. A structured framework for the design process is presented. The obtained model is characterized by a strong hierarchy and concurrency that is why within the design process an iterative approach for specification, verification and validation is propose in order to improve this process. The main properties being verified are presented and the approach is illustrated through an example of a manufacturing production cell.References
C. André, Representation and Analysis of Reactive Behaviors: A Synchronous Approach, in Proc. of the IEEE-SMC Computational Engineering in Systems Applications (CESA 96), Lille, France, July, 1996, pp. 19-29.
C. André, Semantics of SSM (Safe State Machines), Guyancourt, France, April 2003, Available at: http://www.esterel-technologies.com
A. Benveniste, P. Caspi, S. Edwards, N. Halbwachs, P. Le Guernic, and R. de Simone, The Synchronous Languages Twelve Years Later, in Proc. of the IEEE, 91(1), special issue on Embedded Systems, pp. 64-83, 2003.
G. Berry, G. Gonthier, The Esterel synchronous programming language: design, semantics, implementation, Science of Computer Programming, Vol. 19(2), pp. 87-152, 1992. http://dx.doi.org/10.1016/0167-6423(92)90005-V
G. Berry, The constructive semantics of pure Esterel Draft version 3, 1999, Available at: http://www.esterel-technologies.com
A. Bouali, XEVE an Esterel Verification Environment, in Proc. 14th Int. Conf. on Computer Aided Verification CAV'98, LNCS, UBC, Vancouver, Canada, June 1998.
Esterel StudioTM, Available at: http://www.esterel-technologies.com.
N. Halbawachs, F. Lagnier and P. Raymond, Synchronous observers and the verification of reactive systems, in Proc. of AMAST'93, 1993.
Hamani N, Dangoumau N, Craye E, A comparative study of mode handling approaches, in Proc. of the 35th International Conference on Computers & Industrial Engineering (CIE 05), Istanbul Turkey, June 19-22, 2005.
N. Hamani, A contribution to modeling and verification for mode handling of manufacturing systems, PhD dissertation, Ecole Centrale de Lille, France, 2005 [in french].
N. Hamani, N. Dangoumau, E. Craye, Functional modeling for mode handling of Flexible Manufacturing Systems, in Proc. 12th IFAC Symposium on Information Control Problems in Manufacturing, Saint Etienne, France, 2006. http://dx.doi.org/10.1016/b978-008044654-7/50179-5
D. Harel, StateCharts: a visual approach for complex systems, Science of Computer Programming, Vol. 8, nˇr3, pp. 231-275, 1987.
K.L. McMillan, Symbolic Model Checking, Kluwer Academic Publishers, 1993. http://dx.doi.org/10.1007/978-1-4615-3190-6
J.M. Roussel, and J.J. Lesage, Validation and Verification of Grafcet using finite state machines, in Proc. of IMACS-IEEE Multiconference on Computational Engineering in Systems Applications, Lille, France, 1996, pp. 758-764.
Published
Issue
Section
License
ONLINE OPEN ACCES: Acces to full text of each article and each issue are allowed for free in respect of Attribution-NonCommercial 4.0 International (CC BY-NC 4.0.
You are free to:
-Share: copy and redistribute the material in any medium or format;
-Adapt: remix, transform, and build upon the material.
The licensor cannot revoke these freedoms as long as you follow the license terms.
DISCLAIMER: The author(s) of each article appearing in International Journal of Computers Communications & Control is/are solely responsible for the content thereof; the publication of an article shall not constitute or be deemed to constitute any representation by the Editors or Agora University Press that the data presented therein are original, correct or sufficient to support the conclusions reached or that the experiment design or methodology is adequate.
