Obtaining Plant Models for Formal Verification Tasks from 3D CAD Models: Which is the Best Approach?

Abstract:

The use of analysis techniques for industrial controller’s analysis, such as Simulation and Formal Verification, is sometimes complex on industrial context. This complexity is due to the fact that such techniques require sometimes big investment in highly qualified human resources that have sufficient theoretical knowledge in those domains. This paper aims, mainly, to show that it is possible to improve the implementation and industrial using of such techniques, by facilitating their application. As any mechatronic system needs to be modeled by using CAD models, these models could be used, in a systematic way, by these companies in order to increase the use of such techniques for the analysis of industrial controllers. For this purpose, it is discussed, in the paper, the best way to systematize these procedures, and this paper describes, only, the first step of a complex process and promotes a discussion of the main difficulties that can be found and a possibility for handle those difficulties is presented. A case study is presented in order to illustrate how to obtain a plant model for formal verification purposes from an original 3D CAD model.

• Periodical: Advanced Materials Research (Volume 630)
• Pages: 283-290
• DOI: https://doi.org/10.4028/www.scientific.net/AMR.630.283
• Online since: December 2012
• Authors: Edgar Lobo, João Fertuzinhos, João P.M.A. Silva, José Machado
• Keywords: CAD Modeling, Formal Verification, Mechatronic Systems Safety, Safe Controllers Design

References

[1] Machado, J., E. Seabra, J.C. Campos, F. Soares, and C.P. Leão, Safe controllers design for industrial automation systems. Computers & Industrial Engineering, 2011. 60(4): pp.635-653.

DOI: 10.1016/j.cie.2010.12.020

[2] Baresi, L., M. Mauri, and M. Pezzè, PLCTOOLS: Graph Transformation Meets PLC Design. Electronic Notes in Theoretical Computer Science, 2002. 72(2): p.79.

DOI: 10.1016/s1571-0661(05)80532-8

[3] Rankin, D.J. and J. Jin, A Hardware-in-the-Loop Simulation Platform for the Verification and Validation of Safety Control Systems. Nuclear Science, IEEE Transactions on, 2011. 58(2): pp.468-478.

DOI: 10.1109/tns.2010.2103325

[4] Machado, J., B. Denis, and J.J. Lesage. A generic approach to build plant models for DES verification purposes. in Discrete Event Systems, 2006 8th International Workshop on. (2006).

DOI: 10.1109/wodes.2006.382508

[5] Machado, J., Influence de la prise en compte d'un modèle de processus en vérification formelle des Systémes à Evénements Discrets, in Departamento de Engenharia Mecânica2006, Ecole Normale Supérieure de Cachan: Cachan. p.176.

[6] Preusse, S. and H.M. Hanisch. Verifying functional and non-functional properties of manufacturing control systems. in Dependable Control of Discrete Systems (DCDS), 2011 3rd International Workshop on. (2011).

DOI: 10.1109/dcds.2011.5970316

[7] S. Preuße, C. Gerber, and H. -M. Hanisch, Hardware-In-The-Loop Simulation and Verification of Manufacturing Control Systems, in Proceedings of 18th IFAC World Congress2011: Milano, Italy.

[8] Moon, I., G.J. Powers, J.R. Burch, and E.M. Clarke, Automatic verification of sequential control systems using temporal logic. AIChE Journal, 1992. 38(1): pp.67-75.

DOI: 10.1002/aic.690380107

[9] Alur, R. and D.L. Dill, A theory of timed automata. Theor. Comput. Sci., 1994. 126(2): pp.183-235.

[10] Behrmann, G., A. David, K.G. Larsen, P. Pettersson, and W. Yi, Developing UPPAAL over 15 years. Software: Practice and Experience, 2011. 41(2): pp.133-142.

DOI: 10.1002/spe.1006

[11] Clarke, E.M., E.A. Emerson, and A.P. Sistla, Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst., 1986. 8(2): pp.244-263.

DOI: 10.1145/5397.5399

[12] Systems, F.A.A. Festo®. [cited 2012 April 04th]; Available from: http: /www. festo. com/net/startpage.

[13] Pahl, G. and W. Beitz, Engineering Design – A Systematic Approach1996, London.

[14] Pugh, S., Total design : integrated methods for successful product engineering1991: Harlow : Prentice Hall, cop. (1991).

[15] Drejer, A. and A. Gudmundsson, Exploring the concept of multiple product development via an action research project. Integrated Manufacturing Systems, 2003. Vol. 14: pp.208-220.

DOI: 10.1108/09576060310463163

[16] Ulrich, K.T. and S.D. Eppinger, Product Design and Development2000, New York,: McGraw-Hill.

[17] Jones, J.C., Design Methods, ed. ed1992, New York: Van Nostrand ReinHold.

[18] Kreith, Mechanical Engineering Handbook1999, Boca Raton: CRC Press.

[19] Tim Bray, T., Extensible Markup Language (XML) 1. 0 (Second Edition).

[20] Diethers, K. and M. Huhn, Vooduu: Verification of Object-Oriented Designs Using UPPAAL Tools and Algorithms for the Construction and Analysis of Systems, K. Jensen and A. Podelski, Editors. 2004, Springer Berlin / Heidelberg. pp.139-143.

DOI: 10.1007/978-3-540-24730-2_10

[21] Knapp, A., S. Merz, and C. Rauh, Model Checking Timed UML State Machines and Collaborations Formal Techniques in Real-Time and Fault-Tolerant Systems, W. Damm and E. Olderog, Editors. 2002, Springer Berlin / Heidelberg. pp.395-414.

DOI: 10.1007/3-540-45739-9_23

[22] SIEMENS. Solid Edge®. [cited 2012 April]; Available from: http: /www. plm. automation. siemens. com/en_us/products/velocity/solidedge.

[23] Systèmes, D. CATIA®. [cited 2012 April]; Available from: http: /www. 3ds. com/products/catia/welcome.

[24] Systèmes, D. SOLIDWORKS®. [cited 2012 April]; Available from: http: /www. 3ds. com/products/solidworks/overview.

[25] Yang, J., S. Hang, J. Cho, B. Kim, and H.Y. Lee, An XML-Based Macro Data Representation for a Parametric CAD Model Exchange.

[26] SCRA, STEP APPLICATION HANDBOOK ISO 10303 2006: NORTH CHARLESTON. p.181.

[27] Mandorli, F., H.E. Otto, and F. Kimura, A reference kernel model for feature-based CAD systems supported by conditional attributed rewrite systems, in Proceedings on the second ACM symposium on Solid modeling and applications1993, ACM: Montreal, Quebec, Canada. pp.343-354.

DOI: 10.1145/164360.164468

[28] Choi, G. -H., D. Mun, and S. Han, Exchange of CAD Part Models Based on the Macro-Parametric Approach. International Journal of CAD/CAM, 2002. Vol 2: p.9.

[29] Sivaloganathan, S., T.M.M. Shahin, M. Cross, and M. Lawrence, A hybrid systematic and conventional approach for the design and development of a product: a case study. Design Studies, January 2000. vol 21(1): pp.59-74.

DOI: 10.1016/s0142-694x(99)00004-6

[30] Anderl, R. and R. Mendgen, Analyzing and optimizing constraint structures in complex parametric CAD models. Geometric Constraint Solving and Applications, ed. B. . In: Brüderlin, Roller, D. (eds. ), , , , 1998, Berlin Heidelberg Springer-Verlag.

DOI: 10.1007/978-3-642-58898-3_4

[31] ISO10303. 2003; Available from: www. tc184-sc4. org.

[32] Silva, J.P.M.A., M.S. Pais, and A.A.C. Monteiro, Dados, comunicação e informação técnica na fabricação mecânica, in XIV Congreso Internacional de Ingeniería Gráfica, INGEGRAF, Editor 2002: Santander, Spain.

[33] Pierra, G., Context-Explication in Conceptual Ontologies: The PLIB Approach, in Proceedings of CE20032003: Madeira.