nach oben

Journal of Intelligent Manufacturing

Erschienen in:

01.10.2014

Automated formal verification for flexible manufacturing systems

verfasst von: E. Carpanzano, L. Ferrucci, D. Mandrioli, M. Mazzolini, A. Morzenti, M. Rossi

Erschienen in: Journal of Intelligent Manufacturing | Ausgabe 5/2014

Einloggen

Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.

search-config

KI-gestützte Suche

Aus

Abstract

We present an effective approach to perform formal verification of properties of interest of production systems whose behavior is modeled through Stateflow diagrams. The approach hinges on a semantics of Stateflow diagrams given in terms of formulae of a metric temporal logic. The semantics has been implemented in a fully automated tool through which users can define a wide range of properties of interest and then check if they hold for the system. We illustrate the approach and the use of the tool through a realistic case study. The verification technique allowed us to uncover a previously undetected error in the design of the system.

Vorheriger Artikel An approach to monitoring quality in manufacturing using supervised machine learning on product state data

Nächster Artikel Application of the classical levels of intelligence to structuring the control system in an automated distribution centre

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Alur, R., & Henzinger, T. (1999). Reactive modules. Formal Methods in System Design, 15, 7–48.CrossRef

Ballarino, A., & Carpanzano, E. (2002). Modular automation systems design using the IEC 61499 standard and the simulink/stateflow toolboxes. In Proceedings of the asme Japan–USA symposium on flexible automation.

Basile, F., Chiacchio, P., Vittorini, V., & Mazzocca, N. (2004). Modeling and logic controller specification of flexible manufacturing systems using behavioral traces and petri net building blocks. Journal of Intelligent Manufacturing, 15, 351–371.CrossRef

Bersani, M., Frigeri, A., Morzenti, A., Pradella, M., Rossi, M., & SanPietro, P. (2010) Bounded reachability for temporal logic over constraint systems. In Proceedings of the 17th international symposium on temporal representation and reasoning (TIME), pp 43–50.

Brusaferri, A., Ballarino, A., & Capanzano, E. (2011). Reconfigurable knowledge-based control solutions for responsive manufacturing systems. Studies in Informatics and Control (SIC), 20, 31–42.

Ciapessoni, E., Crivelli, E., Coen-Porisini, A., Mandrioli, D., Mirandola, P., & Morzenti, A. (1999). From formal models to formally-based methods: An industrial experience. ACM Transactions on Software Engineering and Methodology, pp. 79–113.

Cimatti, A., Clarke, E. M., Giunchiglia, E., Giunchiglia, F., Pistore, M., Roveri, et al. (2002). NuSMV 2: An opensource tool for symbolic model checking. In Proceedings of the 14th internationl conference on computer aided verification (CAV), pp. 359–364.

Esteve, M. A., Katoen, J. P., Nguyen, V. Y., Postma, B., & Yushtein, Y. (2012). Formal correctness, safety, dependability, and performance analysis of a satellite. In Proceedings of the international conference on software engineering (ICSE), pp. 1022–1031.

Furia, C. A., Mandrioli, D., Morzenti, A., & Rossi, M. (2012). Modeling time in computing. EATCS Monographs in Theoretical Computer Science. Berlin: Springer.

Gourcuff, V., DeSmet, O., & Faure, J. (2008). Improving large sized plc programs verification using abstractions. In Proceedings of the 17th IFAC world congress.

Hanisch, H. M., Lobov, A., Lastra, J. M., Tuokko, R., & Vyatkin, V. (2006). Formal validation of intelligent-automated production systems: towards industrial applications. International Journal of Manufacturing Technology and Management, 8(1), 75–106.

Harel, D. (1987). Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3), 231–274.CrossRef

Harel, D., & Naamad, A. (1996). The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4), 293–333.CrossRef

IEC. (2003). International Standard IEC61131-3, Programming Lan- guages for Programmable Controllers. International Electro-technical Commission, (IEC), 2nd edn.

IEC. (2005). International Standard IEC61499, Function Blocks, Part 1–4. International Electro-technical Commission, (IEC), 1st edn.

ISaGRAF IT. (2012). Isagraf6 developer web site and online documentation. http://www.isagraf.com.

Khalgui, M., Mosbahi, O., Hanisch, H. M., & Li, Z. (2012). A multi-agent architectural solution for coherent distributed reconfigurations of function blocks. Journal of Intelligent Manufacturing, 23, 2531–2549.CrossRef

Klein, S., Weng, X., Frey, G., Lesage, J., & Litz, L. (2002). Controller design for an FMS using signal interpreted Petri nets and SFC. In Proceedings of the American control conference, pp. 4141–4146.

Levi, F. (2000). Compositional verification of quantitative properties of statecharts. Journal of Logic and Computation, 11(6), 829–878.CrossRef

Lewis, R. (2001). Modelling control systems using iec 61499. applying function blocks to distributed systems. IEEE Publishing.

Mathworks. (2011). Stateflow online documentation. http://www.mathworks.it/help/toolbox/stateflow/.

Mazzolini, M., Brusaferri, A., Carpanzano, E. (2010). Model-checking based verification approach for advanced industrial automation solutions. In Proceedings of the international conference on emerging technologies and factory automation, pp 1–8.

Pradella, M., Morzenti, A., & San Pietro, P. (2008). Refining real-time system specifications through bounded model- and satisfiability-checking. In Proceedings of the 23rd IEEE/ACM international conference on automated software engineering, pp. 119–127.

Pranevicius, H. (1998). Formal specification and analysis of distributed systems. Journal of Intelligent Manufacturing, 9, 559–569.CrossRef

Thapa, D., Park, C., Dangol, S., & Wang, G. (2006). III-phase verification and validation of IEC standard programmable logic controller. In Proceedings of the IEEE international conference on computational intelligence for modelling control and automation, pp. 111–111.

Vyatkin, V. (2011). IEC 61499 as enabler of distributed and intelligent automation: State-of-the-art review. IEEE Transactions on Industrial Informatics, 7(4), 768–781.CrossRef

Vyatkin, V., & Hanisch, H. M. (2003). Verification of distributed control systems in intelligent manufacturing. Journal of Intelligent Manufacturing, 14, 123–136.CrossRef

Vyatkin, V., Hanisch, H. M., & Pfeiffer, T. (2003). Object-oriented modular place/transition formalism for systematic modeling and validation of industrial automation systems. In Proceedings of the IEEE international conference on industrial informatics, pp. 224–232.

Wang, J., & Deng, Y. (1999). Incremental modeling and verification of flexible manufacturing systems. Journal of Intelligent Manufacturing, 10, 485–502.CrossRef

Zhang, D., & Anosike, A. (2012). Modelling and simulation of dynamically integrated manufacturing systems. Journal of Intelligent Manufacturing, 23, 2367–2382.CrossRef

Titel: Automated formal verification for flexible manufacturing systems
verfasst von: E. Carpanzano
L. Ferrucci
D. Mandrioli
M. Mazzolini
A. Morzenti
M. Rossi
Publikationsdatum: 01.10.2014
Verlag: Springer US
Erschienen in: Journal of Intelligent Manufacturing / Ausgabe 5/2014
Print ISSN: 0956-5515
Elektronische ISSN: 1572-8145
DOI: https://doi.org/10.1007/s10845-013-0760-z

Premium Partner

Marktübersichten

Die im Laufe eines Jahres in der „adhäsion“ veröffentlichten Marktübersichten helfen Anwendern verschiedenster Branchen, sich einen gezielten Überblick über Lieferantenangebote zu verschaffen.

Zur Marktübersicht

Springer Professional

Abstract

Bitte loggen Sie sich ein, um Zugang zu Ihrer Lizenz zu erhalten.

Sie haben noch keine Lizenz? Dann Informieren Sie sich jetzt über unsere Produkte:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Weitere Artikel der Ausgabe 5/2014

The construction of a hospital disease tracking and control system with a disease infection probability model

Manufacturing intelligence and innovation for digital manufacturing and operational excellence

Predictive control architecture for real-time image moments based servoing of robot manipulators

Therblig-based energy demand modeling methodology of machining process to support intelligent manufacturing

Optimization technique by genetic algorithms for international logistics

Hybrid sampling strategy-based multiobjective evolutionary algorithm for process planning and scheduling problem

Premium Partner

Marktübersichten