Automated formal verification for flexible manufacturing systems
- 392 Downloads
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.
KeywordsFormal methods Formal verification Bounded model checking
- 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
- 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
- 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
- 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
- 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
- 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
- Furia, C. A., Mandrioli, D., Morzenti, A., & Rossi, M. (2012). Modeling time in computing. EATCS Monographs in Theoretical Computer Science. Berlin: Springer.Google Scholar
- 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
- 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
- IEC. (2003). International Standard IEC61131-3, Programming Lan- guages for Programmable Controllers. International Electro-technical Commission, (IEC), 2nd edn.Google Scholar
- IEC. (2005). International Standard IEC61499, Function Blocks, Part 1–4. International Electro-technical Commission, (IEC), 1st edn.Google Scholar
- ISaGRAF IT. (2012). Isagraf6 developer web site and online documentation. http://www.isagraf.com.
- 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
- Lewis, R. (2001). Modelling control systems using iec 61499. applying function blocks to distributed systems. IEEE Publishing.Google Scholar
- 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.Google Scholar
- 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
- 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
- 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