[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic

  • General
  • Special Issue TACAS 2018
  • Published:
International Journal on Software Tools for Technology Transfer Aims and scope Submit manuscript

Abstract

We introduce in this paper \(\text {AMT} \; 2.0\), a tool for qualitative and quantitative analysis of hybrid continuous and Boolean signals that combine numerical values and discrete events. The evaluation of the signals is based on rich temporal specifications expressed in extended signal temporal logic, which integrates timed regular expressions within signal temporal logic. The tool features qualitative monitoring (property satisfaction checking), trace diagnostics for explaining and justifying property violations and specification-driven measurement of quantitative features of the signal. We demonstrate the tool functionality on several running examples and case studies, and evaluate its performance.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Fig. 1
Fig. 2
Fig. 3
Fig. 4
Fig. 5
Fig. 6
Fig. 7
Fig. 8
Fig. 9
Fig. 10
Fig. 11
Fig. 12
Fig. 13
Fig. 14
Fig. 15
Fig. 16

Similar content being viewed by others

Notes

  1. We note that \({{\,\mathrm{\uparrow }\,}}p\) and \({{\,\mathrm{\downarrow }\,}}p\) have a slightly different semantics in TRE than in STL. As a consequence, the tool uses keywords start and end to denote \(\uparrow \) and \(\downarrow \) in TREs, instead of keywords rise and fall used in STL formulas.

References

  1. Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)

    Article  MathSciNet  MATH  Google Scholar 

  2. Annpureddy, Y., Liu, C., Fainekos, G.E., Sankaranarayanan, S.: S-taliro: a tool for temporal logic falsification for hybrid systems. In: Tools and Algorithms for the Construction and Analysis of Systems—Proceedings 17th International Conference, TACAS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011, pp. 254–257 (2011)

  3. Asarin, E., Caspi, P., Maler, O.: A Kleene theorem for timed automata. In: Logic in Computer Science (LICS), pp. 160–171 (1997)

  4. Asarin, E., Caspi, P., Maler, O.: Timed regular expressions. J. ACM 49(2), 172–206 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  5. Asarin, E., Donzé, A., Maler, O., Nickovic, D.: Parametric identification of temporal properties. In: Runtime Verification—2nd International Conference, RV 2011, San Francisco, CA, USA, September 27–30, 2011, Revised Selected Papers, pp. 147–160 (2011)

  6. Bartocci, E., Deshmukh, J., Donzé, A., Fainekos, G., Maler, O., Nickovic, D., Sankaranarayanan, S.: Specification-based monitoring of cyber-physical systems: a survey on theory, tools and applications. In: The Handbook of Runtime Verification (2018)

  7. Bartocci, E., Ferrère, T., Manjunath, N., Nickovic, D.: Localizing faults in simulink/stateflow models with STL. In: Proceedings of the 21st International Conference on Hybrid Systems: Computation and Control (part of CPS Week), HSCC 2018, Porto, Portugal, April 11-13, 2018, pp. 197–206 (2018)

  8. Basin, D.A., Krstic, S., Traytel, D.: Almost event-rate independent monitoring of metric dynamic logic. In: Runtime Verification—Proceedings of 17th International Conference, RV 2017, Seattle, WA, USA, September 13–16, 2017, pp. 85–102 (2017)

  9. Calzone, L., Fages, F., Soliman, S.: BIOCHAM: an environment for modeling biological systems and formalizing experimental knowledge. Bioinformatics 22(14), 1805–1807 (2006)

    Article  Google Scholar 

  10. Deshmukh, J.V., Donzé, A., Ghosh, S., Jin, X., Juniwal, G., Seshia, S.A.: Robust online monitoring of signal temporal logic. In: Runtime Verification—Proceedings of 6th International Conference, RV 2015 Vienna, Austria, September 22–25 2015, pp. 55–70 (2015)

  11. Donzé, A.: Breach, a toolbox for verification and parameter synthesis of hybrid systems. In: Proceedings of 22nd International Conference on Computer Aided Verification, CAV 2010, Edinburgh, UK, July 15–19, 2010, pp. 167–170 (2010)

  12. Donzé, A., Maler, O.: Robust satisfaction of temporal logic over real-valued signals. In: Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 92–106 (2010)

  13. Eisner, C., Fisman, D.: A practical introduction to PSL. Springer, Berlin (2006)

    Google Scholar 

  14. Ferrère, T., Maler, O., Nickovic, D.: Trace diagnostics using temporal implicants. In: Automated Technology for Verification and Analysis—Proceedings of 13th International Symposium, ATVA 2015, Shanghai, China, October 12–15, 2015, pp. 241–258 (2015)

  15. Ferrère, T., Maler, O., Nickovic, D., Ulus, D.: Measuring with timed patterns. In: Computer Aided Verification—Proceeding of 27th International Conference, CAV 2015, San Francisco, CA, USA, July 18–24, 2015, Part II, pp. 322–337 (2015)

  16. Ghidella, J., Mosterman, P.: Requirements-based testing in aircraft control design. In: AIAA Modeling and Simulation Technologies Conference and Exhibit, p. 5886 (2005)

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

  18. Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Syst. 2(4), 255–299 (1990)

    Article  Google Scholar 

  19. Maler, O., Nickovic, D.: Monitoring temporal properties of continuous signals. In: Formal techniques, modelling and analysis of timed and fault-tolerant systems. In: Joint International Conferences on Formal Modelling and Analysis of Timed Systems, FORMATS 2004 and Formal Techniques in Real-Time and Fault-Tolerant Systems, FTRTFT 2004, Grenoble, France, September 22–24, 2004, pp. 152–166 (2004)

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

    Article  Google Scholar 

  21. Nguyen, T., Nickovic, D.: Assertion-based monitoring in practice - checking correctness of an automotive sensor interface. Sci. Comput. Program. 118, 40–59 (2016)

    Article  Google Scholar 

  22. Nickovic, D., Lebeltel, O., Maler, O., Ferrère, T., Ulus, D.: AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. In: Tools and Algorithms for the Construction and Analysis of Systems—Proceedings of 24th International Conference, TACAS 2018, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2018, Thessaloniki, Greece, April 14–20, 2018, Part II, pp. 303–319 (2018)

  23. Nickovic, D., Maler, O.: AMT: a property-based monitoring tool for analog systems. In: Proceedings Formal Modeling and Analysis of Timed Systems, 5th International Conference, FORMATS 2007, Salzburg, Austria, October 3–5, 2007, pp. 304–319 (2007)

  24. Ulus, D.: Montre: a tool for monitoring timed regular expressions. In: Computer Aided Verification—Proceedings of 29th International Conference, CAV 2017, Heidelberg, Germany, July 24–28, 2017, Part I, pp. 329–335 (2017)

  25. Ulus, D., Ferrère, T., Asarin, E., Maler, O.: Timed pattern matching. In: Formal Modeling and Analysis of Timed Systems (FORMATS), pp. 222–236 (2014)

  26. Vijayaraghavan, S., Ramanathan, M.: A Practical Guide for System Verilog Assertions. Springer, Berlin (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AIT Austrian Institute of Technology, Seibersdorf, Austria

    Dejan Ničković

  2. Verimag, CNRS/University of Grenoble-Alpes, Grenoble, France

    Olivier Lebeltel & Oded Maler

  3. IST Austria, Klosterneuburg, Austria

    Thomas Ferrère

  4. Boston University, Boston, USA

    Dogan Ulus

Authors
  1. Dejan Ničković
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Olivier Lebeltel
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Oded Maler
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Thomas Ferrère
    View author publications

    You can also search for this author in PubMed Google Scholar

  5. Dogan Ulus
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Dejan Ničković.

Additional information

Publisher's Note

Springer Nature remains neutral with regard to jurisdictional claims in published maps and institutional affiliations.

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Ničković, D., Lebeltel, O., Maler, O. et al. AMT 2.0: qualitative and quantitative trace analysis with extended signal temporal logic. Int J Softw Tools Technol Transfer 22, 741–758 (2020). https://doi.org/10.1007/s10009-020-00582-z

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10009-020-00582-z

Keywords