Skip to main content
SpringerLink
Log in

Assertion-Based Monitoring in Practice – Checking Correctness of an Automotive Sensor Interface

  • Conference paper
Formal Methods for Industrial Critical Systems (FMICS 2014)

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 8718))

Abstract

In this paper, we evaluate the assertion-based monitoring technology for mixed-signal systems by applying it to real-world case study from the automotive domain.

We first motivate the case study by presenting the state-of-the-practice verification and validation work-flow typically used in the automotive industry. We identify the shortcomings of this work-flow, and propose a more rigorous and automated methodology based on monitoring correctness of simulated mixed signal designs with respect to assertions, which formalize in Signal Temporal Logic (STL) the requirements from the design specification.

We apply the assertion-based monitoring framework for mixed signal designs to check the correctness of Distributed System Interface (DSI3) in a modern airbag system-on-chip application. We present all the relevant steps in our proposed work-flow, evaluate the results and discuss the framework’s benefits as well as its identified missing features.

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

Access this chapter

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 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Althoff, M., Rajhans, A., Krogh, B.H., Yaldiz, S., Li, X., Pileggi, L.: Formal verification of phase-locked loops using reachability analysis and continuization. In: Proceedings of the International Conference on Computer-Aided Design, pp. 659–666. IEEE Press (2010)

    Google Scholar 

  2. Alur, R., Courcoubetis, C., Halbwachs, N., Henzinger, T.A., Ho, P.-H., Nicollin, X., Olivero, A., Sifakis, J., Yovine, S.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138(1), 3–34 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  3. Annpureddy, Y., Liu, C., Fainekos, G., Sankaranarayanan, S.: S-TaLiRo: A tool for temporal logic falsification for hybrid systems. In: Abdulla, P.A., Leino, K.R.M. (eds.) TACAS 2011. LNCS, vol. 6605, pp. 254–257. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  4. Bartocci, E., Bortolussi, L., Nenzi, L.: A temporal logic approach to modular design of synthetic biological circuits. In: Gupta, A., Henzinger, T.A. (eds.) CMSB 2013. LNCS, vol. 8130, pp. 164–177. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  5. Bertrane, J.: Static analysis by abstract interpretation of the quasi-synchronous composition of synchronous programs. In: Cousot, R. (ed.) VMCAI 2005. LNCS, vol. 3385, pp. 97–112. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  6. Dang, T., Donzé, A., Maler, O.: Verification of analog and mixed-signal circuits using hybrid system techniques. In: Hu, A.J., Martin, A.K. (eds.) FMCAD 2004. LNCS, vol. 3312, pp. 21–36. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  7. Donzé, A., Fanchon, E., Gattepaille, L.M., Maler, O., Tracqui, P.: Robustness analysis and behavior discrimination in enzymatic reaction networks. PLoS ONE 6(9), e24246 (2011)

    Google Scholar 

  8. Donzé, A.: Breach, A toolbox for verification and parameter synthesis of hybrid systems. In: Touili, T., Cook, B., Jackson, P. (eds.) CAV 2010. LNCS, vol. 6174, pp. 167–170. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  9. Donzé, A., Ferrère, T., Maler, O.: Efficient robust monitoring for STL. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 264–279. Springer, Heidelberg (2013)

    Chapter  Google Scholar 

  10. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Chatterjee, K., Henzinger, T.A. (eds.) FORMATS 2010. LNCS, vol. 6246, pp. 92–106. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  11. Donzé, A., Maler, O., Bartocci, E., Nickovic, D., Grosu, R., Smolka, S.: On temporal logic and signal processing. In: Chakraborty, S., Mukund, M. (eds.) ATVA 2012. LNCS, vol. 7561, pp. 92–106. Springer, Heidelberg (2012)

    Chapter  Google Scholar 

  12. Fainekos, G.E., Pappas, G.J.: Robustness of temporal logic specifications for continuous-time signals. Theor. Comput. Sci. 410(42), 4262–4291 (2009)

    Article  MATH  MathSciNet  Google Scholar 

  13. Frehse, G., Le Guernic, C., Donzé, A., Cotton, S., Ray, R., Lebeltel, O., Ripado, R., Girard, A., Dang, T., Maler, O.: SpaceEx: Scalable verification of hybrid systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 379–395. Springer, Heidelberg (2011)

    Chapter  Google Scholar 

  14. Frehse, G., Krogh, B.H., Rutenbar, R.A.: Verifying analog oscillator circuits using forward/backward abstraction refinement. In: DATE, pp. 257–262. European Design and Automation Association (2006)

    Google Scholar 

  15. Distributed System Interface. DSI3 Bus Standard. DSI Consortium

    Google Scholar 

  16. Jones, K.D., Konrad, V., Nickovic, D.: Analog property checkers: a ddr2 case study. Formal Methods in System Design 36(2), 114–130 (2010)

    Article  MATH  Google Scholar 

  17. Little, S., Walter, D., Jones, K., Myers, C.: Analog/Mixed-signal circuit verification using models generated from simulation traces. In: Namjoshi, K.S., Yoneda, T., Higashino, T., Okamura, Y. (eds.) ATVA 2007. LNCS, vol. 4762, pp. 114–128. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  18. Maler, O., Manna, Z., Pnueli, A.: From timed to hybrid systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, pp. 447–484. Springer, Heidelberg (1992)

    Google Scholar 

  19. 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)

    Chapter  Google Scholar 

  20. Maler, O., Nickovic, D.: Monitoring properties of analog and mixed-signal circuits. STTT 15(3), 247–268 (2013)

    Article  Google Scholar 

  21. Nickovic, D., Maler, O.: AMT: A property-based monitoring tool for analog systems. In: Raskin, J.-F., Thiagarajan, P.S. (eds.) FORMATS 2007. LNCS, vol. 4763, pp. 304–319. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  22. Pnueli, A.: The temporal logic of programs. In: FOCS, pp. 46–57 (1977)

    Google Scholar 

  23. Rizk, A., Batt, G., Fages, F., Soliman, S.: On a continuous degree of satisfaction of temporal logic formulae with applications to systems biology. In: Heiner, M., Uhrmacher, A.M. (eds.) CMSB 2008. LNCS (LNBI), vol. 5307, pp. 251–268. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  24. Steinhorst, S., Hedrich, L.: Model checking of analog systems using an analog specification language. In: DATE, pp. 324–329. ACM (2008)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Infineon Technologies AG, Austria

    Thang Nguyen

  2. AIT Austrian Institute of Technology GmbH, Vienna, Austria

    Dejan Ničković

Authors
  1. Thang Nguyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Dejan Ničković
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Inria, 38330, Montbonnot, France

    Frédéric Lang

  2. Ansaldo STS, 80147, Naples, Italy

    Francesco Flammini

Rights and permissions

Reprints and permissions

Copyright information

© 2014 Springer International Publishing Switzerland

About this paper

Cite this paper

Nguyen, T., Ničković, D. (2014). Assertion-Based Monitoring in Practice – Checking Correctness of an Automotive Sensor Interface. In: Lang, F., Flammini, F. (eds) Formal Methods for Industrial Critical Systems. FMICS 2014. Lecture Notes in Computer Science, vol 8718. Springer, Cham. https://doi.org/10.1007/978-3-319-10702-8_2

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-10702-8_2

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-10701-1

  • Online ISBN: 978-3-319-10702-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation