Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Design, Modeling, and Evaluation of Cyber Physical Systems

CyPhy 2016: Cyber Physical Systems. Design, Modeling, and Evaluation pp 87–100Cite as

Automated Verification of Switched Systems Using Hybrid Identification

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNISA,volume 10107))

Abstract

Verification of switched systems has to include the continuous trajectories as well as the discrete states of the system. For strongly interconnected systems with mutual dependencies it is not sufficient to verify the two system parts individually. It is necessary to examine the combined behaviour in such a setting. The approach presented in this paper is based on the well known concept of using system identification methods for verification which is extended to switched systems. The authors introduce the idea to tackle the verification of complex mechatronical systems as hybrid identification problem. Therefore the specification is given by the user in terms of the parameters of linear dynamic systems and a superimposed state machine. The implemented system under test can be transformed into the same representation using input/output measurement data and a recently developed hybrid identification procedure. Finally it is possible to compare the two representations automatically and calculate a formal statement about the consistency between specification and implementation.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Notes

  1. 1.

    The term “verification” is used in the control engineering sense throughout this paper which is denoted as “conformance testing” in computer science.

References

  1. Transregional collaborative research center “automatic verification and analysis of complex systems (avacs)”. http://www.avacs.org

  2. Abel, A., Reineke, J.: Memin: sat-based exact minimization of incompletely specified mealy machines. In: Proceedings of the IEEE/ACM International Conference on Computer-Aided Design, ICCAD 2015, Austin, TX, USA, 2–6 November 2015, pp. 94–101 (2015)

    Google Scholar 

  3. Alur, R., Dang, T., Ivančić, F.: Reachability analysis of hybrid systems via predicate abstraction. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 35–48. Springer, Heidelberg (2002). doi:10.1007/3-540-45873-5_6

    Chapter  Google Scholar 

  4. Alur, R., Dang, T., Ivančić, F.: Predicate abstraction for reachability analysis of hybrid systems. ACM Trans. Embed. Comput. Syst. 5(1), 152–199 (2006)

    Article  MATH  Google Scholar 

  5. Anta, A., Majumdar, R., Saha, I., Tabuada, P.: Automatic verification of control system implementations. In: Proceedings of the Tenth ACM International Conference on Embedded Software, pp. 9–18 (2010)

    Google Scholar 

  6. Araiza-Illan, D., Eder, K., Richards, A.: Verification of control systems implemented in simulink with assertion checks and theorem proving: a case study. In: 2015 European Control Conference (ECC), pp. 2670–2675, July 2015

    Google Scholar 

  7. Badban, B., Fränzle, M., Peleska, J., Teige, T.: Test automation for hybrid systems. In: Proceedings of the 3rd International Workshop on Software Quality Assurance, SOQUA 2006, pp. 14–21. ACM, New York (2006)

    Google Scholar 

  8. Balluchi, A., Benvenuti, L., di Benedetto, M.D., Pinello, C., Sangiovanni-Vincentelli, A.L.: Automotive engine control and hybrid systems: challenges and opportunities. Proc. IEEE 88(7), 888–912 (2000)

    Article  Google Scholar 

  9. Bhatia, A., Frazzoli, E.: Incremental search methods for reachability analysis of continuous and hybrid systems. In: Alur, R., Pappas, G. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 142–156. Springer, Berlin Heidelberg (2004)

    Chapter  Google Scholar 

  10. Broy, M., Jonsson, B., Katoen, J.-P., Leucker, M., Pretschner, A. (eds.): Model-Based Testing of Reactive Systems: Advanced Lectures. LNCS, vol. 3472. Springer, Heidelberg (2005)

    MATH  Google Scholar 

  11. Chen, W., Chen, W.-T., Saif, M., Li, M.-F., Wu, H.: Simultaneous fault isolation and estimation of lithium-ion batteries via synthesized design of luenberger and learning observers. IEEE Trans. Control Syst. Technol. 22(1), 290–298 (2014)

    Article  Google Scholar 

  12. Dang, T.: Model-based testing of hybrid systems. In: Model-Based Testing for Embedded Systems, chap. 14, pp. 383–424

    Google Scholar 

  13. Denise, A., Gaudel, M.-C., Gouraud, S.-D.: A generic method for statistical testing. In: 15th International Symposium on Software Reliability Engineering, ISSRE 2004, pp. 25–34 (2004)

    Google Scholar 

  14. Diehm, G., Maier, S., Flad, M., Hohmann, S.: An identification method for individual driver steering behaviour modelled by switched affine systems. In: Proceedings of the 52nd IEEE Conference on Decision and Control, pp. 3547–3553 (2013)

    Google Scholar 

  15. Diehm, G., Maier, S., Flad, M., Hohmann, S.: Online identification of individual driver steering behaviour and experimental results. In: Proceedings of the IEEE International Conference on Systems, Man and Cybernetics, pp. 221–227 (2013)

    Google Scholar 

  16. Föllinger, O., Konigorski, U.: Regelungstechnik: Einführung die Methoden und ihre Anwendung, 11, völlig neu bearb. aufl. edn. VDE-Verl., Berlin (2013)

    Google Scholar 

  17. Frank, P.M.: Diagnoseverfahren in der Automatisierungstechnik. at - Automatisierungstechnik, 47–64 (1994)

    Google Scholar 

  18. Holling, D., Pretschner, A., Gemmar, M.: 8cage: lightweight fault-based test generation for simulink. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, pages 859–862. ACM, New York (2014)

    Google Scholar 

  19. Kaner, C.: An introduction to scenario testing (2003)

    Google Scholar 

  20. Lin, L., Poore, J.H., Eschbach, R., Hierons, R.M., Robinson-Mallett, C.: Augmenting sequence enumeration with string-rewriting for requirements analysis and behavioral specification. In: Cortellessa, V., Varró, D. (eds.) FASE 2013. LNCS, vol. 7793, pp. 179–193. Springer, Heidelberg (2013). doi:10.1007/978-3-642-37057-1_13

    Chapter  Google Scholar 

  21. Liu, D., Guo, X., Tang, G., Huang, Z.: Model Validation via System Identification and Hypothesis Test. Springer, Heidelberg (2012)

    Book  Google Scholar 

  22. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS/FTRTFT-2004. LNCS, vol. 3253, pp. 152–166. Springer, Heidelberg (2004). doi:10.1007/978-3-540-30206-3_12

    Chapter  Google Scholar 

  23. Matinnejad, R., Nejati, S., Briand, L., Bruckmann, T., Poull, C.: Proceedings of the 5th International Symposium on Search based software engineering, SSBSE 2013, St. Petersburg, Russia, 24–26 August 2013, pp. 141–157 (2013)

    Google Scholar 

  24. Matinnejad, R., Nejati, S., Briand, L., Bruckmann, T., Poull, C.: Search-based automated testing of continuous controllers: framework, tool support, and case studies. Inf. Softw. Technol. 57, 705–722 (2015)

    Article  Google Scholar 

  25. Matinnejad, R., Nejati, S., Briand, L.C., Bruckmann, T.: Automated test suite generation for time-continuous simulink models, pp. 595–606 (2016)

    Google Scholar 

  26. Pajic, M., Park, J., Lee, I., Pappas, G.J., Sokolsky, O.: Automatic verification of linear controller software. In: Proceedings of the 12th International Conference on Embedded Software, EMSOFT 2015, pp. 217–226. IEEE Press, Piscataway (2015)

    Google Scholar 

  27. Schneider, J.: Tracking down root causes of defects in simulink models. In: Proceedings of the 29th ACM/IEEE International Conference on Automated Software Engineering, ASE 2014, pp. 599–604. ACM, New York (2014)

    Google Scholar 

  28. Schupp, S., Ábrahám, E., Chen, X., Makhlouf, I., Frehse, G., Sankaranarayanan, S., Kowalewski, S.: Current challenges in the verification of hybrid systems. In: Berger, C., Mousavi, M.R. (eds.) CyPhy 2015. LNCS, vol. 9361, pp. 8–24. Springer, Heidelberg (2015). doi:10.1007/978-3-319-25141-7_2

    Chapter  Google Scholar 

  29. Simon, S.: Objektorientierte Methoden zum automatisierten Entwurf von modell-basierten Diagnosesystemen. PhD thesis, Berlin, 2015. Zugl.: Kaiserslautern, Techn. Univ., Diss. (2015)

    Google Scholar 

  30. Utting, M., Pretschner, A., Legeard, B.: A taxonomy of model-based testing (2006)

    Google Scholar 

  31. Yordanov, B., Belta, C.: Formal analysis of discrete-time piecewise affine systems. IEEE Trans. Autom. Control 55(12), 2834–2840 (2010)

    Article  MathSciNet  Google Scholar 

  32. Zander-Nowicka, J.: Model-based testing of real-time embedded systems in the automotive domain (2009)

    Google Scholar 

  33. Zhao, F., Koutsoukos, X., Haussecker, H., Reich, J., Cheung, P.: Monitoring and fault diagnosis of hybrid systems. IEEE Trans. Syst. Man Cybern. Part B (Cybern.) 35(6), 1225–1240 (2005)

    Article  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institute of Control Systems, Karlsruhe Institute of Technology, 76131, Karlsruhe, Germany

    Stefan Schwab & Sören Hohmann

  2. ITK-Engineering, 70565, Stuttgart, Germany

    Bernd Holzmüller

Authors
  1. Stefan Schwab
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Bernd Holzmüller
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Sören Hohmann
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Stefan Schwab .

Editor information

Editors and Affiliations

  1. University of Gothenburg, Gothenburg, Sweden

    Christian Berger

  2. Halmstad University, Halmstad, Sweden

    Mohammad Reza Mousavi

  3. Aalborg University, Aalborg, Denmark

    Rafael Wisniewski

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Schwab, S., Holzmüller, B., Hohmann, S. (2017). Automated Verification of Switched Systems Using Hybrid Identification. In: Berger, C., Mousavi, M., Wisniewski, R. (eds) Cyber Physical Systems. Design, Modeling, and Evaluation. CyPhy 2016. Lecture Notes in Computer Science(), vol 10107. Springer, Cham. https://doi.org/10.1007/978-3-319-51738-4_7

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-51738-4_7

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-51737-7

  • Online ISBN: 978-3-319-51738-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation