nach oben

Erschienen in:

2019 | OriginalPaper | Buchkapitel

Formal Verification: Focused on the Verification Using a Plant Model

verfasst von : Joel Galvão, Cedrico Oliveira, Helena Lopes, Laura Tiainen

Erschienen in: Innovation, Engineering and Entrepreneurship

Verlag: Springer International Publishing

Einloggen

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

search-config

KI-gestützte Suche

Aus

Abstract

The main goal of this paper is present a review and discussion about the option of using plant models in formal verification techniques. Relevant works in the field considering different approaches are reviewed and the importance of choosing the level of detail correctly is discussed. Although exists few works about this topic, the studies revealed the necessity and importance to consider the plant model in formal verification.

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

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

Jetzt informieren

Vorheriges Kapitel Decentralized Adaptive Suboptimal LQ Control in Microsoft Excel VBA

Nächstes Kapitel Mechatronic Design and Control of a Robotic System for Inspection Tasks

Considine, D.M., Considine, G.D.: Standard Handbook of Industrial Automation. Chapman & Hall, New York (1986)MATH

Baresi, L., Carmeli, S., Monti, A., Pezzè, M.: PLC programming languages: a formal approach. In: Proceedings of Automation 1998 (1998)

Canadas, N., Machado, J., Soares, F.: Simulation of cyber physical systems behaviour using timed plant models. Mechatronics, 0–1 (2017). https://doi.org/10.1016/j.mechatronics.2017.10.009

Chioran, D., Machado, J.M.: Design of a mechatronic system for application of hardware-in-the-loop simulation technique (2011)

Enoiu, E.P., Sundmark, D., Pettersson, P.: Model-based test suite generation for function block diagrams using the uppaal model checker. In: 2013 IEEE Sixth International Conference on Software Testing, Verification and Validation Workshops (ICSTW), pp 158–167 (2013)

Barth, M., Fay, A.: Automated generation of simulation models for control code tests. Control Eng. Pract. 21, 218–230 (2013)CrossRef

Zhang, Y., Dong, Y., Hong, H., Zhang, F.: Code formal verification of operation system. Int. J. Comput. Netw. Inf. Secur. 2, 10–18 (2010)

Campos, J., Machado, J.: A specification patterns system for discrete event systems analysis. Int. J. Adv. Robot. Syst. 10, 315 (2013). https://doi.org/10.5772/56412CrossRef

Meenakshi, B.: Formal verification. Resonance 10, 26–38 (2005)CrossRef

10.

Alur, R., Courcoubetis, C., Dill, D.: Model-checking in dense real-time. Inf. Comput. 104, 2–34 (1993)MathSciNetCrossRef

11.

Fikes, R.E., Nilsson, N.J.: Strips: A new approach to the application of theorem proving to problem solving. Artif. Intell. 2, 189–208 (1971). https://doi.org/10.1016/0004-3702(71)90010-5CrossRefMATH

12.

Ćengić, G., Åkesson, K.: On formal analysis of IEC 61499 applications, Part A: Modeling. IEEE Trans. Industr. Inf. 6, 136–144 (2010)CrossRef

13.

Vyatkin, V.: IEC 61499 Function Blocks for Embedded and Distributed Control Systems Design. ISA-Instrumentation, Systems, and Automation Society, Oneida (2007)

14.

John, K.-H., Tiegelkamp, M.: IEC 61131-3: Programming Industrial Automation Systems: Concepts and Programming Languages, Requirements for Programming Systems, Decision-Making Aids. Springer Science & Business Media, Heidelberg (2010)

15.

Frey, G., Litz, L.: Formal methods in PLC programming. In: 2000 IEEE International Conference on Systems, Man, and Cybernetics, Nashville, USA, pp. 2431–2436 (2000)

16.

Vyatkin, V., Hanisch, H.-M.: Verification of distributed control systems in intelligent manufacturing. J. Intell. Manuf. 14, 123–136 (2003)CrossRef

17.

Roussel, J.-M., Denis, B.: Safety properties verification of ladder diagram programs. J. Eur. des Systèmes Autom. 36, 905–917 (2002)

18.

Machado, J.M.: Influence de la prise en compte d’un modèle de processus en vérification formelle des Systèmes à Evénements Discrets. Universidade do Minho (2006)

19.

Machado, J.J.B., Denis, B., Lesage, J.-J., et al.: Logic controllers dependability verification using a plant model. In: Proceedings of the 3rd IFAC Workshop on Discrete-Event System Design, DESDes 2006, Rydzyna, Poland, 26–28 September 2006

20.

Kunz, G., Machado, J., Perondi, E.: Using timed automata for modeling, simulating and verifying networked systems controller’s specifications. Neural Comput. Appl. 28, 1031–1041 (2017)CrossRef

21.

Plummer, A.R.: Model-in-the-loop testing. Proc. Inst. Mech. Eng. Part I J. Syst. Control Eng. 220, 183–199 (2006). https://doi.org/10.1243/09596518JSCE207CrossRef

22.

Alur, R., Dill, D.: Automata for modeling real-time systems. In: Proceedings of Seventeenth International Colloquium on Automata, Languages, and Programming, pp. 322–335 (1990)

23.

Pacheco, R., Gonzalez, L., Intriago, M.: Issues to be considered on obtaining plant models for formal verification purposes. In: IOP Conference Series: Materials Science and Engineering, vol. 147 (2016). https://doi.org/10.1088/1757-899X/147/1/012050

24.

Machado, J., Denis, B.: A generic approach to build plant models for DES verification purposes, pp. 407–412 (2006)

25.

Machado, J., Galvão, J., Fernandes, A.: Formal verification considering a systematic modeling approach for function blocks. J. Braz. Soc. Mech. Sci. Eng. 39, 4107–4113 (2017). https://doi.org/10.1007/s40430-017-0893-7CrossRef

26.

Buzhinsky, I., Vyatkin, V.: Plant model inference for closed-loop verification of control systems : initial explorations. In: 2016 IEEE 14th International Conference on Industrial Informatics (INDIN), pp. 736–739 (2015)

27.

Vyatkin, V.V.: Net condition/event systems (NCES) (2005). http://homepages.engineering.auckland.ac.nz/~vyatkin/nces/net_condition_event_systems.htm. Accessed 18 Jun 2015

28.

Vyatkin, V., Starke, P., Hanisch, H.-M.: ViVe and SESA model checkers (2007). http://homepages.engineering.auckland.ac.nz/~vyatkin/tools/modelchekers.html. Accessed 19 Mar 2015

29.

Sorouri, M., Patil, S., Salcic, Z., Vyatkin, V.: Software composition and distributed operation scheduling in modular automated machines. IEEE Trans. Industr. Inf. 11, 865–878 (2015). https://doi.org/10.1109/TII.2015.2430836CrossRef

30.

Carpanzano, E., Ferrucci, L., Mandrioli, D., et al.: Automated formal verification for flexible manufacturing systems. J. Intell. Manuf. 25, 1181–1195 (2014)CrossRef

31.

Lasi, H., Fettke, P., Kemper, H.G., et al.: Industry 4.0. Bus. Inf. Syst. Eng. 6, 239–242 (2014). https://doi.org/10.1007/s12599-014-0334-4CrossRef

32.

Kunz, G., Machado, J., Perondi, E., Vyatkin, V.: A formal methodology for accomplishing IEC 61850 real-time communication requirements. IEEE Trans. Industr. Electron. 64, 6582–6590 (2017). https://doi.org/10.1109/TIE.2017.2682042CrossRef

33.

Khaitan, S.K., McCalley, J.D.: Design techniques and applications of cyber physical systems: a survey. IEEE Syst. J. 9, 350–365 (2015). https://doi.org/10.1109/JSYST.2014.2322503CrossRef

Titel: Formal Verification: Focused on the Verification Using a Plant Model
verfasst von: Joel Galvão
Cedrico Oliveira
Helena Lopes
Laura Tiainen
Verlag: Springer International Publishing
Buch: Innovation, Engineering and Entrepreneurship
Print ISBN: 978-3-319-91333-9

Electronic ISBN: 978-3-319-91334-6

Copyright-Jahr: 2019
DOI: https://doi.org/10.1007/978-3-319-91334-6_18

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"

Springer Professional "Wirtschaft"

Premium Partner