Journal of Intelligent Manufacturing

, Volume 25, Issue 5, pp 1181–1195 | Cite as

Automated formal verification for flexible manufacturing systems

  • E. Carpanzano
  • L. Ferrucci
  • D. Mandrioli
  • M. Mazzolini
  • A. Morzenti
  • M. Rossi


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.


Formal methods Formal verification Bounded model checking 


  1. Alur, R., & Henzinger, T. (1999). Reactive modules. Formal Methods in System Design, 15, 7–48.CrossRefGoogle Scholar
  2. 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.Google Scholar
  3. 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.CrossRefGoogle Scholar
  4. 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.Google Scholar
  5. 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.Google Scholar
  6. 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.Google Scholar
  7. 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.Google Scholar
  8. 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.Google Scholar
  9. Furia, C. A., Mandrioli, D., Morzenti, A., & Rossi, M. (2012). Modeling time in computing. EATCS Monographs in Theoretical Computer Science. Berlin: Springer.Google Scholar
  10. Gourcuff, V., DeSmet, O., & Faure, J. (2008). Improving large sized plc programs verification using abstractions. In Proceedings of the 17th IFAC world congress.Google Scholar
  11. 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.Google Scholar
  12. Harel, D. (1987). Statecharts: A visual formalism for complex systems. Science of Computer Programming, 8(3), 231–274.CrossRefGoogle Scholar
  13. Harel, D., & Naamad, A. (1996). The STATEMATE semantics of statecharts. ACM Transactions on Software Engineering and Methodology, 5(4), 293–333.CrossRefGoogle Scholar
  14. IEC. (2003). International Standard IEC61131-3, Programming Lan- guages for Programmable Controllers. International Electro-technical Commission, (IEC), 2nd edn.Google Scholar
  15. IEC. (2005). International Standard IEC61499, Function Blocks, Part 1–4. International Electro-technical Commission, (IEC), 1st edn.Google Scholar
  16. ISaGRAF IT. (2012). Isagraf6 developer web site and online documentation.
  17. 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.CrossRefGoogle Scholar
  18. 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.Google Scholar
  19. Levi, F. (2000). Compositional verification of quantitative properties of statecharts. Journal of Logic and Computation, 11(6), 829–878.CrossRefGoogle Scholar
  20. Lewis, R. (2001). Modelling control systems using iec 61499. applying function blocks to distributed systems. IEEE Publishing.Google Scholar
  21. Mathworks. (2011). Stateflow online documentation.
  22. 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.Google Scholar
  23. 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.Google Scholar
  24. Pranevicius, H. (1998). Formal specification and analysis of distributed systems. Journal of Intelligent Manufacturing, 9, 559–569.CrossRefGoogle Scholar
  25. 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.Google Scholar
  26. 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.CrossRefGoogle Scholar
  27. Vyatkin, V., & Hanisch, H. M. (2003). Verification of distributed control systems in intelligent manufacturing. Journal of Intelligent Manufacturing, 14, 123–136.CrossRefGoogle Scholar
  28. 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.Google Scholar
  29. Wang, J., & Deng, Y. (1999). Incremental modeling and verification of flexible manufacturing systems. Journal of Intelligent Manufacturing, 10, 485–502.CrossRefGoogle Scholar
  30. Zhang, D., & Anosike, A. (2012). Modelling and simulation of dynamically integrated manufacturing systems. Journal of Intelligent Manufacturing, 23, 2367–2382.CrossRefGoogle Scholar

Copyright information

© Springer Science+Business Media New York 2013

Authors and Affiliations

  • E. Carpanzano
    • 1
  • L. Ferrucci
    • 2
  • D. Mandrioli
    • 2
  • M. Mazzolini
    • 3
  • A. Morzenti
    • 2
  • M. Rossi
    • 2
  1. 1.Istituto di Sistemi e Tecnologie per la Produzione Sostenibile Scuola Universitaria Professionale della Svizzera ItalianaMannoSwitzerland
  2. 2.Politecnico di MilanoMilanItaly
  3. 3.Synesis ConsortiumKilometro Rosso Science and Technology ParkBergamoItaly

Personalised recommendations