Skip to main content
Top

2017 | OriginalPaper | Chapter

Validation of Industrial Cyber-Physical Systems: An Application to HVAC Systems

Authors : Thao Dang, Alie El-Din Mady, Menouer Boubekeur, Rajesh Kumar, Mark Moulin

Published in: Complex Systems Design & Management

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config
loading …

Abstract

We describe a validation approach for Simulink models of industrial cyber-physical systems (CPS), based on an adaptation of a coverage-guided test generation method for hybrid systems. Modelling an industrial CPS requires integrating heterogeneous components, which introduces high complexity in model verification. Using Simulink, which has become a de-facto industrial tool, heterogeneity comes from combining different formalisms (Simulink blocks, Stateflow diagrams, Matlab and C functions, etc.) and mixing different types of dynamics (discrete, continuous). Since the interactions between such components are often too complex to be faithfully captured in an existing mathematical modelling paradigm, we resort to treating them as black box systems while trying to exploit as much as possible a-priori knowledge about them. We first describe our approach: extracting from a Simulink model the information to define the main ingredients of the test generation framework, in particular environment inputs in which faults could be injected and critical states that require good coverage. We then illustrate the approach with an industrial model of an HVAC (Heating, Ventilation and Air Conditioning) system.

Dont have a licence yet? Then find out more about our products and how to get one now:

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!

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!

Literature
1.
go back to reference Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. ENTCS 109, 43–56 (2004)MATH Agrawal, A., Simon, G., Karsai, G.: Semantic translation of Simulink/Stateflow models to hybrid automata using graph transformations. ENTCS 109, 43–56 (2004)MATH
2.
go back to reference Arrieta, A., Sagardui, G., Etxeberria, L.: A model-based testing methodology for the systematic validation of highly configurable cyber-physical systems. In: VALID 2014, vol. 66–72. ARIA XPS Press (2014) Arrieta, A., Sagardui, G., Etxeberria, L.: A model-based testing methodology for the systematic validation of highly configurable cyber-physical systems. In: VALID 2014, vol. 66–72. ARIA XPS Press (2014)
3.
go back to reference Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. In: SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems (2012) Bouissou, O., Chapoutot, A.: An operational semantics for Simulink’s simulation engine. In: SIGPLAN/SIGBED Conference on Languages, Compilers and Tools for Embedded Systems (2012)
4.
go back to reference Beck, J., Chen, W.W.L.: Irregularities of distribution. Cambridge University Press, Acta Arithmetica (1997)MATH Beck, J., Chen, W.W.L.: Irregularities of distribution. Cambridge University Press, Acta Arithmetica (1997)MATH
5.
go back to reference Dang, T.: Model-based testing of hybrid systems. In: Model-Based Testing for Embedded Systems, CRC Press (2011) Dang, T.: Model-based testing of hybrid systems. In: Model-Based Testing for Embedded Systems, CRC Press (2011)
6.
go back to reference Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods Syst. Des. 34(2), 183–213 (2009)CrossRefMATH Dang, T., Nahhal, T.: Coverage-guided test generation for continuous and hybrid systems. Formal Methods Syst. Des. 34(2), 183–213 (2009)CrossRefMATH
7.
go back to reference Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proceedings of International Conference on Computer Aided Verification, CAV’10, pp. 167–170. Springer (2010) Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proceedings of International Conference on Computer Aided Verification, CAV’10, pp. 167–170. Springer (2010)
8.
go back to reference Donzé, A., Maler, A.: Robust satisfaction of temporal logic over real-valued signals. In: Formal Modeling and Analysis of Timed Systems—8th International Conference, FORMATS 2010, LNCS 6246, pp. 92–106. Springer (2010) Donzé, A., Maler, A.: Robust satisfaction of temporal logic over real-valued signals. In: Formal Modeling and Analysis of Timed Systems—8th International Conference, FORMATS 2010, LNCS 6246, pp. 92–106. Springer (2010)
9.
go back to reference Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: NASA Formal Methods NFM 2015, LNCS 9058, pp. 127–142. Springer (2015) Dreossi, T., Dang, T., Donzé, A., Kapinski, J., Jin, X., Deshmukh, J.V.: Efficient guiding strategies for testing of temporal properties of hybrid systems. In: NASA Formal Methods NFM 2015, LNCS 9058, pp. 127–142. Springer (2015)
10.
go back to reference Hoxha, B., Bach, H., Abbas, H., Dokhanchi, A., Kobayashi, Y., Fainekos, G.: Towards formal specification visualization for testing and monitoring of cyber-physical systems. In: International Workshop on Design and Implementation of Formal Tools and Systems (2014) Hoxha, B., Bach, H., Abbas, H., Dokhanchi, A., Kobayashi, Y., Fainekos, G.: Towards formal specification visualization for testing and monitoring of cyber-physical systems. In: International Workshop on Design and Implementation of Formal Tools and Systems (2014)
11.
go back to reference LaValle, S., Kuffner, J.: Rapidly-exploring random trees: Progress and prospects. In: Workshop on the Algorithmic Foundations of Robotics (2000) LaValle, S., Kuffner, J.: Rapidly-exploring random trees: Progress and prospects. In: Workshop on the Algorithmic Foundations of Robotics (2000)
12.
go back to reference Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. In: Hybrid Systems: Computation and Control (HSCC), LNCS, vol. 3414, pp. 25–53. Springer (2005) Lee, E.A., Zheng, H.: Operational semantics of hybrid systems. In: Hybrid Systems: Computation and Control (HSCC), LNCS, vol. 3414, pp. 25–53. Springer (2005)
13.
go back to reference Mady, A.E.D., Provan, G.M., Boubekeur, M.: Towards integrated hybrid modelling and simulation platform for building automation systems; First models for a simple HVAC system. In: Information Technology & Telecommunication Conference (IT&T), pp. 191–199 (2009) Mady, A.E.D., Provan, G.M., Boubekeur, M.: Towards integrated hybrid modelling and simulation platform for building automation systems; First models for a simple HVAC system. In: Information Technology & Telecommunication Conference (IT&T), pp. 191–199 (2009)
14.
go back to reference Mady, A.E.D., Provan, G.M., Ryan, C., Brown, K.N.: Stochastic model predictive controller for the integration of building use and temperature regulation. In: Conference of Association for the Advancement of Artificial Intelligence (AAAI), pp. 1371–1376 (2011) Mady, A.E.D., Provan, G.M., Ryan, C., Brown, K.N.: Stochastic model predictive controller for the integration of building use and temperature regulation. In: Conference of Association for the Advancement of Artificial Intelligence (AAAI), pp. 1371–1376 (2011)
15.
go back to reference Satpathy, M., Yeolekar, A., Ramesh, S.: Randomized directed testing (redirect) for Simulink/Stateflow models. In: Proceedings of the 8th ACM International Conference on Embedded Software, EMSOFT ’08, pp. 217–226. ACM (2008) Satpathy, M., Yeolekar, A., Ramesh, S.: Randomized directed testing (redirect) for Simulink/Stateflow models. In: Proceedings of the 8th ACM International Conference on Embedded Software, EMSOFT ’08, pp. 217–226. ACM (2008)
16.
go back to reference Scenarios for a clean energy future: Interlaboratory working group on energy-effcient and clean-energy technologies (2000). NREL/TP-620-29379; ORNL/CON-476; LBNL-44029 Scenarios for a clean energy future: Interlaboratory working group on energy-effcient and clean-energy technologies (2000). NREL/TP-620-29379; ORNL/CON-476; LBNL-44029
17.
go back to reference Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embedded Comput. Syst. 4(4), 779–818 (2005)CrossRef Tripakis, S., Sofronis, C., Caspi, P., Curic, A.: Translating discrete-time Simulink to Lustre. ACM Trans. Embedded Comput. Syst. 4(4), 779–818 (2005)CrossRef
Metadata
Title
Validation of Industrial Cyber-Physical Systems: An Application to HVAC Systems
Authors
Thao Dang
Alie El-Din Mady
Menouer Boubekeur
Rajesh Kumar
Mark Moulin
Copyright Year
2017
DOI
https://doi.org/10.1007/978-3-319-49103-5_5