Advertisement

Verifying Event-Based Timing Constraints by Translation into Presburger Formulae

  • Björn LisperEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10471)

Abstract

Abstract modeling of timing properties is often based on events. An event can be seen as a sequence of times. Timing constraints can then be expressed as constraints on events: an example is the TADL2 language that has been developed in the automotive domain.

Event-based constraints can express timing properties of implementations as well as timing requirements. An important step in timing verification is then to show that any events that comply with the properties of the implementation, i.e., that describe the timings of its possible behaviours, also satisfy the requirements.

Real-time software is often organised as a set of periodically repeating tasks, especially in domains with time-critical systems like automotive and avionics. This implementation naturally yields periodic events, where each event occurrence belongs to a periodically repeating time window. An interesting question is then: if some events are periodic in this fashion, will they then fulfil a timing constraint that describes a timing requirement? We show, for a number of TADL2 timing constraints, how to translate this implication into an equivalent Presburger formula. Since Presburger logic is decidable, this yields an automated method to decide whether the periodic implementation satisfies the timing requirements or not. Initial experiments with a Presburger solver indicate that the method is practical.

Notes

Acknowledgments

This work was partially supported by VINNOVA through the ITEA2 TIMMO-2-USE and ITEA3 ASSUME projects. We would also like to thank Johan Nordlander for interesting discussions.

References

  1. 1.
    Abadi, M., Lamport, L.: An old-fashioned recipe for real time. ACM Trans. Program. Lang. Syst. 16(5), 1543–1571 (1994)CrossRefGoogle Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceeding of Logic in Computer Science, pp. 414–425. IEEE (1990)Google Scholar
  3. 3.
    Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41(1), 181–203 (1994)CrossRefzbMATHMathSciNetGoogle Scholar
  4. 4.
    Amon, T., Borriello, G., Hu, T., Liu, J.: Symbolic timing verification of timing diagrams using Presburger formulas. In: Proceeding of 34th Annual Design Automation Conference, pp. 226–231. ACM, New York (1997)Google Scholar
  5. 5.
    André, C., Mallet, F.: Clock constraints in UML/MARTE CCSL. Research report, INRIA, May 2008Google Scholar
  6. 6.
    AUTOSAR: Homepage of the AUTOSAR project (2009). www.autosar.org/
  7. 7.
    AUTOSAR: Specification of timing extensions (2011). www.autosar.org/
  8. 8.
    Baruah, S., Buttazzo, G., Gorinsky, S., Lipari, G.: Scheduling periodic task systems to minimize output jitter. In: Proceeding of Sixth International Conference on Real-Time Computing Systems and Applications (RTCSA 1999), pp. 62–69 (1999)Google Scholar
  9. 9.
    Beringer, S., Wehrheim, H.: Verification of AUTOSAR software architectures with timed automata. In: Beek, M.H., Gnesi, S., Knapp, A. (eds.) FMICS/AVoCS 2016. LNCS, vol. 9933, pp. 189–204. Springer, Cham (2016). doi: 10.1007/978-3-319-45943-1_13 CrossRefGoogle Scholar
  10. 10.
    Blom, H., Feng, L., Lönn, H., Nordlander, J., Kuntz, S., Lisper, B., Quinton, S., Hanke, M., Peraldi-Frati, M.A., Goknil, A., Deantoni, J., Defo, G.B., Klobedanz, K., Özhan, M., Honcharova, O.: D11 language syntax, semantics, metamodel v2. Technical report, August 2012. https://itea3.org/project/timmo-2-use.html
  11. 11.
    Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)CrossRefzbMATHMathSciNetGoogle Scholar
  12. 12.
    Cuenot, P., et al.: 11 The EAST-ADL architecture description language for automotive embedded software. In: Giese, H., Karsai, G., Lee, E., Rumpe, B., Schätz, B. (eds.) MBEERTS 2007. LNCS, vol. 6100, pp. 297–307. Springer, Heidelberg (2010). doi: 10.1007/978-3-642-16277-0_11 CrossRefGoogle Scholar
  13. 13.
    Ge, N., Pantel, M.: Time properties verification framework for UML-MARTE safety critical real-time systems. In: Vallecillo, A., Tolvanen, J.-P., Kindler, E., Störrle, H., Kolovos, D. (eds.) ECMFA 2012. LNCS, vol. 7349, pp. 352–367. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-31491-9_27 CrossRefGoogle Scholar
  14. 14.
    Hune, T., Romijn, J., Stoelinga, M., Vaandrager, F.W.: Linear parametric model checking of timed automata. J. Log. Algebr. Program. 52–53, 183–220 (2002). http://dx.doi.org/10.1016/S1567-8326(02)00037-1
  15. 15.
    Johansson, R., Frey, P., Jonsson, J., Nordlander, J., Pathan, R.M., Feiertag, N., Schlager, M., Espinoza, H., Richter, K., Kuntz, S., Lönn, H., Kolagari, R.T., Blom, H.: TADL: timing augmented description language, version 2. Technical report, October 2009Google Scholar
  16. 16.
    Larsen, K.G., Pettersson, P., Yi, W.: UPPAAL in a nutshell. Int. J. Softw. Tools Technol. Transfer 1, 134–152 (1997)CrossRefzbMATHGoogle Scholar
  17. 17.
    Lisper, B., Nordlander, J.: A simple and flexible timing constraint logic. In: Margaria, T., Steffen, B. (eds.) ISoLA 2012. LNCS, vol. 7610, pp. 80–95. Springer, Heidelberg (2012). doi: 10.1007/978-3-642-34032-1_12 CrossRefGoogle Scholar
  18. 18.
    Liu, C., Layland, J.: Scheduling algorithms for multiprogramming in a hard-real-time environment. J. ACM 20(1), 46–61 (1973)CrossRefzbMATHMathSciNetGoogle Scholar
  19. 19.
    Mok, A.K.: Fundamental design problems of distributed systems for the hard-real-time environment. Ph.D. thesis, Massachusetts Institute of Technology, May 1983Google Scholar
  20. 20.
    UML profile for MARTE: modeling and analysis of real-time embedded systems. Technical report, OMG, November 2009Google Scholar
  21. 21.
    Suryadevara, J.: Validating EAST-ADL timing constraints using UPPAAL. In: Proceeding 39th Euromicro Conference on Software Engineering and Advanced Applications (SEAA), September 2013. http://www.es.mdh.se/publications/2988-22
  22. 22.
    Verdoolaege, S.: barvinok: user guide. Technical report, January 2016. barvinok.gforge.inria.fr/barvinok.pdf
  23. 23.
    Yin, L., Mallet, F., Liu, J.: Verification of MARTE/CCSL time requirements in Promela/SPIN. In: Proceeding of 16th IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2011), pp. 65–74, April 2011Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.School of Innovation, Design, and EngineeringMälardalen UniversityVästeråsSweden

Personalised recommendations