Skip to main content

2017 | OriginalPaper | Buchkapitel

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

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

Erschienen in: Complex Systems Design & Management

Verlag: Springer International Publishing

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

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.

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!

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!

Literatur
1.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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.
Zurück zum Zitat 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
Metadaten
Titel
Validation of Industrial Cyber-Physical Systems: An Application to HVAC Systems
verfasst von
Thao Dang
Alie El-Din Mady
Menouer Boubekeur
Rajesh Kumar
Mark Moulin
Copyright-Jahr
2017
DOI
https://doi.org/10.1007/978-3-319-49103-5_5

Neuer Inhalt