Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Formal Techniques for Safety-Critical Systems

FTSCS 2014: Formal Techniques for Safety-Critical Systems pp 62–75Cite as

Checking Integral Real-Time Automata for Extended Linear Duration Invariants

  • Conference paper
  • First Online:

  • 572 Accesses

Part of the book series: Communications in Computer and Information Science ((CCIS,volume 476))

Abstract

Linear duration invariants are important safety properties of real-time systems. They are represented as linear inequalities of integrated durations of system states and form a decidable subclass of Duration Calculus formulas. The problem of whether a real-time automaton satisfies a linear duration invariant can be transformed into a finite number of linear programming problems. In this paper, extended linear duration invariants, which are linear inequalities of integrals of physical quantities that characterize real-time systems, are introduced. The semantics of extended linear duration invariants is defined by introducing integral real-time automata whose states are labeled with a finite number of integrable functions. The problem of checking an integral real-time automaton for an extended linear duration invariant is transformed into a finite number of nonlinear programming problems which can be solved easily. A case study of a reaction tank is discussed to demonstrate the effectiveness of the technique introduced in the paper.

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

References

  1. Chaochen, Z., Hoare, C.A.R., Ravn, A.P.: A calculus of durations. Inf. Process. Lett. 40(5), 269–276 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  2. Zhou, C.: Linear duration invariants. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, pp. 86–109. Springer, Heidelberg (1994)

    Chapter  Google Scholar 

  3. Kesten, Y., Pnueli, A., Sifakis, J., Yovine, S.: Integration graphs: a class of decidable hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 179–208. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  4. Braberman, V.A., Van Hung, D.: On checking timed automata for linear duration invariants. In: Proceedings of the 19th Real-Time Systems Symposium RTSS 1998, pp. 264–273. IEEE Computer Society Press, Los Alamitos (1998)

    Google Scholar 

  5. Zhang, M., Van Hung, D., Liu, Z.: Verification of linear duration invariants by model checking CTL properties. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 395–409. Springer, Heidelberg (2008)

    Google Scholar 

  6. Zhang, M., Liu, Z., Zhan, N.: Model checking linear duration invariants of networks of automata. In: Arbab, F., Sirjani, M. (eds.) FSEN 2009. LNCS, vol. 5961, pp. 244–259. Springer, Heidelberg (2010)

    Chapter  Google Scholar 

  7. Thai, P.H., Van Hung, D.: Verifying linear duration constraints of timed automata. In: Liu, Z., Araki, K. (eds.) ICTAC 2004. LNCS, vol. 3407, pp. 295–309. Springer, Heidelberg (2005)

    Google Scholar 

  8. Ravn, A.P., Rischel, H., Hansen, K.M.: Specifying and verifying requirements of real-time systems. IEEE Trans. Softw. Eng. 19(1), 41–55 (1993)

    Article  Google Scholar 

  9. Chaochen, Z., Xiaoshan, L.: A mean-value duration calculus. In: Roscoe, A.W. (ed.) A Classical Mind, Essays in Honour of C. A. R. Hoare, pp. 431–451. Prentice Hall International, Englewood Cliffs (1994)

    Google Scholar 

  10. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MATH  MathSciNet  Google Scholar 

  11. S\(\phi \)rensen, E.V., Ravn A.P., Rischel H.: Control Program for a Gas Burner: Part 1: Informal Requirements, ProCoS Case Study 1. ProCoS I, ESPRIT BRA 3104, Report No. ID/DTH EVS2, Department of Computer Science, Technical University of Denmark, Lyngby (1990)

    Google Scholar 

  12. Alur, R., Courcoubetis, C., Henzinger, T.A., Ho, P.-H.: Hybrid automata: an algorithmic approach to the specification and verification of hybrid systems. In: Grossman, R.L., Ravn, A.P., Rischel, H., Nerode, A. (eds.) HS 1991 and HS 1992. LNCS, vol. 736, pp. 209–229. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  13. Chaochen, Z., Hansen, M.R.: Duration Calculus. A Formal Approach to Real-Time Systems. Springer, Heidelberg (2004)

    Book  MATH  Google Scholar 

  14. Chaochen, Z., Hansen, M.R., Sestoft, P.: Decidability and undecidability results for duration calculus. In: Enjalbert, P., Finkel, A., Wagner, K.W. (eds.) (STACS 93). LNCS, vol. 665, pp. 58–68. Springer-Verlag, Heidelberg (1993)

    Google Scholar 

  15. Chaochen, Z., Ravn, A.P., Hansen, M.R.: An extended duration calculus for hybrid real-time systems. In: Grossman, R.L., Nerode, A., Ravn, A.P., Rischel, H. (eds.) Hybrid Systems. LNCS, vol. 736, pp. 36–59. Springer, Heidelberg (1993)

    Chapter  Google Scholar 

  16. Zhang, H., Wang, S.: Global optimization of separable objective functions on convex polyhedra via piecewise-linear approximation. J. Comput. Appl. Math. 197, 212–217 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  17. Behrmann, G., Larsen, K.G., Rasmussen, J.I.: Priced timed automata: algorithms and applications. In: de Boer, F.S., Bonsangue, M.M., Graf, S., de Roever, W.-P. (eds.) FMCO 2004. LNCS, vol. 3657, pp. 162–182. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  18. Bouyer, P.: Weighted timed automata: model-checking and games. In: Brookes, S., Mislove (eds.) Proceedings of the 22nd Annual Conference on Mathematical Foundations of Programming Semantics, Electronic Notes in Theoretical Computer Science, vol. 158, pp. 3–17 (2006)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Faculty of Mathematics, Kim Il Sung University, Pyongyang, Democratic People’s Republic of Korea

    Changil Choe & Song Han

  2. Faculty of Physics, Kim Il Sung University, Pyongyang, Democratic People’s Republic of Korea

    Univan Ahn

Authors
  1. Changil Choe
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Univan Ahn
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Song Han
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Changil Choe .

Editor information

Editors and Affiliations

  1. National Institute of Advanced Industrial Science and Technology, Amagasaki, Japan

    Cyrille Artho

  2. University of Oslo, Oslo, Norway

    Peter Csaba Ölveczky

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer International Publishing Switzerland

About this paper

Cite this paper

Choe, C., Ahn, U., Han, S. (2015). Checking Integral Real-Time Automata for Extended Linear Duration Invariants. In: Artho, C., Ölveczky, P. (eds) Formal Techniques for Safety-Critical Systems. FTSCS 2014. Communications in Computer and Information Science, vol 476. Springer, Cham. https://doi.org/10.1007/978-3-319-17581-2_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-17581-2_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-17580-5

  • Online ISBN: 978-3-319-17581-2

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation