Abstract
In the past few years two research groups of Politecnico di Milano, whose activities were centered on Formal Methods for the production of critical software and on industrial manufacturing systems, respectively, have carried out a joint research project that, among other things, aimed at introducing the use of formal methods in the design and analysis phases of industrial production systems (and especially of so-called Flexible Manufacturing Systems, FMSs) as a complementary tool to the ones used in the current practice of the field. This paper reports on the challenges that the research groups faced during the project, and on the lessons that have been learned in the process.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Bruccoleri, M., La Diega, S.N., Perrone, G.: Object-oriented approach for flexible manufacturing control systems analysis and design using the Unified Modeling Language. Int. Journal of Flexible Manufacturing Systems 15(3), 195–216 (2003)
Matta, A., Semeraro, Q., Tolio, T.: A framework for long term capacity decisions in advanced manufacturing systems. In: Matta, A., Semeraro, Q. (eds.) Design of Advanced Manufacturing Systems, Springer, Heidelberg (2005)
Zhou, M., Venkatesh, K.: Modeling, Simulation, and Control of Flexible Manufacturing Systems: A Petri Net Approach. World Scientific, Singapore (1999)
Wang, J., Deng, Y.: Incremental modeling and verification of flexible manufacturing systems. Journal of Intelligent Manufacturing 10(6), 485–502 (1999)
Hatono, I., Yamagata, K., Tamura, H.: Modeling and online scheduling of flexible manufacturing systems using stochastic petri nets. IEEE Transactions on Software Engineering 17(2), 126–132 (1991)
Flake, S., Mueller, W., Pape, U., Ruf, J.: Specification and formal verification of temporal properties of production automation systems. In: Ehrig, H., Damm, W., Desel, J., Große-Rhode, M., Reif, W., Schnieder, E., Westkämper, E. (eds.) INT 2004. LNCS, vol. 3147, pp. 206–226. Springer, Heidelberg (2004)
Matta, A., Furia, C., Rossi, M.: Semi-formal and formal models applied to flexible manufacturing systems. In: Aykanat, C., Dayar, T., Körpeoğlu, İ. (eds.) ISCIS 2004. LNCS, vol. 3280, pp. 718–728. Springer, Heidelberg (2004)
Starr, P.J.: Integration of simulation and analytical submodels for supporting manufacturing decisions. Int. J. of Production Research 29, 1733–1746 (1991)
Ciapessoni, E., Coen-Porisini, A., Crivelli, E., Mandrioli, D., Mirandola, P., Morzenti, A.: From formal models to formally-based methods: an industrial experience. ACM Trans. on Software Engineering and Methodology 8(1), 79–113 (1999)
Matta, A., Tolio, T., Tomasella, M., Zanchi, P.: A detailed uml model for general flexible manufacturing systems. In: Proc. of ICME 2004, pp. 113–118 (2004)
Ghezzi, C., Jazayeri, M., Mandrioli, D.: Fundamentals of Software Engineering, 2nd edn. Prentice-Hall, Englewood Cliffs (2001)
Leone, F.: Specifica e analisi di un flexible manufacturing system. Elaborato di laurea, Politecnico di Milano (in Italian) (2005)
Clarke, E., Grunberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)
Morzenti, A., Mandrioli, D., Ghezzi, C.: A model parametric real-time logic. ACM Transactions on Programming Languages and Systems 14(4), 521–573 (1992)
Gargantini, A., Morzenti, A.: Automated deductive requirement analysis of critical systems. ACM Trans. on Software Eng. and Methodology 10(3), 255–307 (2001)
Morzenti, A., Pradella, M., San Pietro, P., Spoletini, P.: Model-checking trio specifications in SPIN. In: Araki, K., Gnesi, S., Mandrioli, D. (eds.) FME 2003. LNCS, vol. 2805, pp. 542–561. Springer, Heidelberg (2003)
Holzmann, G.: The SPIN Model Checker, Primer and Reference Manual. Addison-Wesley, Reading (2003)
Spoletini, P., Tomasella, M., Matta, A., Rossi, M.: Formal verification in analysis and design of production systems. In: Proc. of ICME 2006, pp. 367–372 (2006)
Ghezzi, C., Mandrioli, D.: The challenges of software engineering education. In: Inverardi, P., Jazayeri, M. (eds.) ICSE 2005. LNCS, vol. 4309, pp. 115–127. Springer, Heidelberg (2006)
Knight, J.C., Leveson, N.G.: Software and higher education. Communications of the ACM 49(1), 160 (2006)
Bourque, P., Dupuis, R. (eds.): Guide to the Software Engineering Book of Knowledge. IEEE Computer Society Press, Los Alamitos (2004)
Lethbridge, T., LeBlanc, R., Sobel, A.K., Hilburn, T., Diaz-Herrera, J.: SE2004: Recommendations for undergraduate software engineering curricula. IEEE Software 23(6), 19–25 (2006)
International Council on Systems Engineering (INCOSE): Guide to the systems engineering body of knowledge – G2SEBoK, online at http://g2sebok.incose.org
Furia, C.A., Rossi, M., Strunk, E.A., Mandrioli, D., Knight, J.C.: Raising formal methods to the requirements level. Technical Report TR 2006.64, Politecnico di Milano (2006)
Pradella, M., Rossi, M., Mandrioli, D.: ArchiTRIO: A UML-compatible language for architectural description and its formal semantics. In: Wang, F. (ed.) FORTE 2005. LNCS, vol. 3731, pp. 381–395. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Matta, A., Rossi, M., Spoletini, P., Mandrioli, D., Semeraro, Q., Tolio, T. (2007). FM for FMS: Lessons Learned While Applying Formal Methods to the Study of Flexible Manufacturing Systems. In: Jones, C.B., Liu, Z., Woodcock, J. (eds) Theoretical Aspects of Computing – ICTAC 2007. ICTAC 2007. Lecture Notes in Computer Science, vol 4711. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-75292-9_25
Download citation
DOI: https://doi.org/10.1007/978-3-540-75292-9_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-75290-5
Online ISBN: 978-3-540-75292-9
eBook Packages: Computer ScienceComputer Science (R0)