Skip to main content
SpringerLink
Log in

Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata

  • Conference paper
  • First Online:
Book cover Formal Methods: Foundations and Applications (SBMF 2021)

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

Included in the following conference series:

Abstract

We present an approach for automatic translation of tock-CSP into Timed Automata (TA) to facilitate using Uppaal in reasoning about temporal specifications of tock-CSP models. The process algebra tock-CSP provides textual notations for modelling discrete-time behaviours, with the support of tools for automatic verification. Automatic verification of TA with a graphical notation is supported by Uppaal. The two approaches provide diverse facilities for automatic verification. For instance, liveness requirements are difficult to specify with the constructs of tock-CSP, but they are easy to specify and verify in Uppaal. We have developed a translation technique based on rules and a tool for translating tock-CSP into a network of small TAs for capturing the compositional structure of tock-CSP. For validating the rules, we begin with an experimental approach based on finite approximations of trace sets. Then, we consider using structural induction to establish the correctness.

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 44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 59.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

Notes

  1. 1.

    Here, the event close is asynchronisation event using the CSP operator ([|Event|]) for synchronising multiple concurrent processes, such that all the processes have to synchronise on the all the elements of the set Event before they can proceed.

  2. 2.

    A TA with linear transitions only, no branches.

  3. 3.

    Also, tock-CSP inherits the operator interrupt (\(/\backslash \)) from CSP, which allows a process to shut down another and takes over the control. For instance, initially the process (\( P /\backslash Q\)) behaves as P but at any time before its termination if the process Q performs a visible action, the process P hands over the control to the process Q. Therefore, the process P terminates and the whole process (\( P /\backslash Q \)) behaves as Q.

  4. 4.

    We use terminating actions where a TA needs to communicate a successful termination for another TA to proceed. For instance, in translating sequential composition , the process begins only after successful termination of the process

  5. 5.

    The term initials describe the first visible events of a process.

  6. 6.

    TA = \((L, l_0, C, A, E, I)\) where L is a set of locations, \(l_0\) is the initial location, C is a set of clocks, A is a set of actions, E is a set of edges and I is an invariant.

References

  1. A repository of this work. https://github.com/ahagmj/TemporalReasoning.git

  2. Abba, A.: Temporal reasoning about robotics applications: refinement and temporal logic. Ph.D. thesis, The University of York (2021)

    Google Scholar 

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

    Google Scholar 

  4. Back, R.: On correct refinement of programs. J. Comput. Syst. Sci. 23(1), 49–68 (1981)

    Article  MathSciNet  Google Scholar 

  5. Behrmann, G., David, A., Larsen, K.G., Håkansson, J., Petterson, P., Wang, Y., Hendriks, M.: UPPAAL 4.0. Third Int. Conf. Quant. Eval. Syst. QEST 2006 pp. 125–126 (2006). https://doi.org/10.1109/QEST.2006.59

  6. Bouyer, P.: Model-checking timed temporal logics. Electr. Notes Theor. Comput. Sci. 231, 323–341 (2009)

    Article  MathSciNet  Google Scholar 

  7. Bouyer, P.: An introduction to timed automata. In: Seatzu, C., Silva M., van Schuppen J. (eds) Control of Discrete-Event Systems. Lecture Notes in Control and Information Sciences, vol. 433, pp. 79–94. Springer, London (2011). https://doi.org/10.1007/978-1-4471-4276-8_9

  8. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finite-state concurrent systems using temporal logic specifications. ACM Trans. Program. Lang. Syst. (TOPLAS) 8(2), 244–263 (1986)

    Article  Google Scholar 

  9. Dong, J.S., Hao, P., Qin, S., Sun, J., Yi, W.: Timed automata patterns. IEEE Trans. Softw. Eng. 34(6), 844–859 (2008)

    Article  Google Scholar 

  10. Dong, J.S., Hao, P., Sun, J., Zhang, X.: A Reasoning method for timed CSP based on constraint solving. In: Liu, Z., He, J. (eds.) ICFEM 2006. LNCS, vol. 4260, pp. 342–359. Springer, Heidelberg (2006). https://doi.org/10.1007/11901433_19

    Chapter  Google Scholar 

  11. Evans, N., Schneider, S.: Analysing time dependent security properties in CSP using PVS. In: European Symposium on Research in Computer Security. pp. 222–237. Springer (2000)

    Google Scholar 

  12. de Freitas, A.F.: From Circus to Java: Implementation and verification of a translation strategy. Master’s thesis, University of York (2005)

    Google Scholar 

  13. Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3: a parallel refinement checker for CSP. Int. J. Softw. Tools Technol, Transf. 18, 149–167 (2016)

    Google Scholar 

  14. Göthel, T., Glesner, S.: Automatic validation of infinite real-time systems. In: 2013 1st FME Workshop on Formal Methods in Software Engineering (FormaliSE), pp. 57–63. IEEE (2013)

    Google Scholar 

  15. Hansen, D., Leuschel, M.: Translating TLA+ to B for validation with ProB. In: International Conference on Integrated Formal Methods, pp. 24–38. Springer (2012)

    Google Scholar 

  16. Hansen, D., Leuschel, M.: Translating B to TLA+ for validation with TLC. In: International Conference on Abstract State Machines, Alloy, B, TLA, VDM, and Z, pp. 40–55. Springer (2014)

    Google Scholar 

  17. Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)

    Article  Google Scholar 

  18. Hutton, G.: Programming in Haskell. Cambridge University Press, Cambridge (2016)

    Google Scholar 

  19. Isobe, Y., Moller, F., Nguyen, H.N., Roggenbach, M.: Safety and line capacity in railways – an approach in timed CSP. In: Derrick, J., Gnesi, S., Latella, D., Treharne, H. (eds.) IFM 2012. LNCS, vol. 7321, pp. 54–68. Springer, Heidelberg (2012). https://doi.org/10.1007/978-3-642-30729-4_5

    Chapter  Google Scholar 

  20. Kahani, N., Bagherzadeh, M., Cordy, J.R., Dingel, J., Varró, D.: Survey and classification of model transformation tools. Softw. Syst. Model. 18(4), 2361–2397 (2018). https://doi.org/10.1007/s10270-018-0665-6

    Article  Google Scholar 

  21. Khattri, M.: Translating timed automata to tock-CSP. In: Proceedings of the 10th IASTED International Conference on Software Engineering, SE 2011 (2011)

    Google Scholar 

  22. Lindstrom, B., Pettersson, P., Offutt, J.: Generating trace-sets for model-based testing. In: The 18th IEEE International Symposium on Software Reliability (ISSRE’07), pp. 171–180. IEEE (2007)

    Google Scholar 

  23. Lowe, G.: Specification of communicating processes: temporal logic versus refusals-based refinement. Form Aspect. Comput. 20(3), 277–294 (2008)

    Article  MathSciNet  Google Scholar 

  24. Mens, T., Van Gorp, P.: A taxonomy of model transformation. Electr. Rotes Theoret. Comput. Sci. 152, 125–142 (2006)

    Article  Google Scholar 

  25. Miyazawa, A., Ribeiro, P., Li, W., Cavalcanti, A., Timmis, J., Woodcock, J.: RoboChart: a State-Machine Notation for Modelling and Verification of Mobile and Autonomous Robots. Tech. Rep. pp. 1–18 (2016)

    Google Scholar 

  26. Nielson, H.R., Nielson, F.: Semantics with Applications: an Appetizer. Springer Science & Business Media, London (2007)

    Google Scholar 

  27. Nogueira, S., Sampaio, A., Mota, A.: Guided test generation from CSP models. In: International Colloquium on Theoretical Aspects of Computing. pp. 258–273. Springer, Cham (2008). https://doi.org/10.1007/978-3-030-85315-0

  28. Oliveira, M.V.M.: Formal derivation of state-rich reactive programs using Circus. Ph.D. thesis, University of York (2005)

    Google Scholar 

  29. Ouaknine, J.: Discrete analysis of continuous behaviour in real-time concurrent systems. Ph.D. thesis, University of Oxford (2000)

    Google Scholar 

  30. Ouaknine, J., Worrell, J.: Timed-CSP = closed timed \(\varepsilon \)-automata. Nordic J. Comput. 10(2), 99–133 (2003)

    MathSciNet  MATH  Google Scholar 

  31. Roscoe, A.W.: Understanding Concurrent Systems. Springer Science & Business Media, London (2010)

    Google Scholar 

  32. Roscoe, A., Hoare, C., Bird, R.: The theory and practice of concurrency. 2005. Revised edition. Only available online (2005)

    Google Scholar 

  33. Schneider, S.: Concurrent and real time systems: the CSP approach. In: World Scientific Proceedings Series on Computer Engineering and Information Science (2010)

    Google Scholar 

  34. Sun, J., Liu, Y., Dong, J.S., Liu, Y., Shi, L., André, E.: Modeling and verifying hierarchical real-time systems using stateful Timed-CSP. ACM Trans. Softw. Eng. Methodol. 22(1) (2013). https://doi.org/10.1145/2430536.2430537, https://doi.org/10.1145/2430536.2430537

  35. Sun, J., Liu, Y., Dong, J.S., Pang, J.: PAT: towards flexible verification under fairness. In: Bouajjani, A., Maler, O. (eds.) CAV 2009. LNCS, vol. 5643, pp. 709–714. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-02658-4_59

    Chapter  Google Scholar 

  36. Ye, K., Woodcock, J.: Model checking of state-rich formalism by linking to \(CSP \parallel B\). Int. J. Softw. Tools Technol. Transf. 19(1), 73–96 (2017)

    Article  Google Scholar 

Download references

Acknowledgements

Abba gratefully acknowledges the financial support of Petroleum Technology Development Fund (PTDF). Cavalcanti is funded by the Royal Academy of Engineering grant CiET1718/45 and the UK EPSRC grants EP/M025756/1 and EP/R025479/1.

Author information

Authors and Affiliations

  1. University of York, York, UK

    Abdulrazaq Abba, Ana Cavalcanti & Jeremy Jacob

  2. University of East London, London, UK

    Abdulrazaq Abba

Authors
  1. Abdulrazaq Abba
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ana Cavalcanti
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Jeremy Jacob
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Abdulrazaq Abba .

Editor information

Editors and Affiliations

  1. Departamento de Ciência da Computação, Universidade Federal de Minas Gerais, Belo Horizonte, Minas Gerais, Brazil

    Sérgio Campos

  2. College of Information and Computer Sciences, University of Massachusetts, Amherst, MA, USA

    Marius Minea

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Abba, A., Cavalcanti, A., Jacob, J. (2021). Temporal Reasoning Through Automatic Translation of tock-CSP into Timed Automata. In: Campos, S., Minea, M. (eds) Formal Methods: Foundations and Applications. SBMF 2021. Lecture Notes in Computer Science(), vol 13130. Springer, Cham. https://doi.org/10.1007/978-3-030-92137-8_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-92137-8_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-92136-1

  • Online ISBN: 978-3-030-92137-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation