Towards Automated and Correct Composition of Timed Services

  • Daniel Stöhr
  • Sabine Glesner
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7759)


The design of programs controlling distributed components in safety-critical domains can be very error-prone and time-consuming. Especially in the presence of real-time requirements the correctness with respect to functional and non-functional properties must be guaranteed. To this end, we develop a technique for the automated and correct composition of timed services based on timed i/o automata, the temporal logic TCTL, and planning algorithms based on model checking. Thus, we can speed up the development of controller programs while assuring correctness.


Model Check Goal State Service Composition Planning Domain Temporal Planning 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    David, A., Larsen, K.G., Legay, A., Nyman, U.: Timed I/O Automata: A Complete Specification Theory for Real-time Systems. Science (2010)Google Scholar
  2. 2.
    Gregorio, D., Cambronero, M.E., Pardo, J.J., Cuartero, F.: Automatic generation of Correct Web Services Choreographies and Orchestrations with Model Checking Techniques. In: International Conference on Internet and Web Applications and Services, AICT-ICIW 2006 (2006)Google Scholar
  3. 3.
    Arney, D., Jetley, R., Jones, P., Lee, I., Sokolsky, O.: Formal Methods Based Development of a PCA Infusion Pump Reference Model: Generic Infusion Pump (GIP) Project. In: Joint Workshop on High Confidence Medical Devices, Software and Systems and Medical Device Plug-and-Play Interoperability (2007)Google Scholar
  4. 4.
    Alur, R.: Techniques for Automatic Verification of Real-Time Systems. PhD thesis, Stanford University (1991)Google Scholar
  5. 5.
    Pistore, M., Bettin, R., Traverso, P.: Symbolic techniques for planning with extended goals in non-deterministic domains. In: 6th European Conference on Planning (2001)Google Scholar
  6. 6.
    Wang, F.: REDLIB A Library of Integrated BDD-like Diagrams for Dense-Time Model Verification (2012)Google Scholar
  7. 7.
    Wang, F.: Efficient verification of timed automata with BDD-like data structures. International Journal on Software Tools for Technology Transfer 6(1), 77–97 (2004)CrossRefGoogle Scholar
  8. 8.
    Pistore, M., Traverso, P., Bertoli, P.: Automated Composition of Web Services by Planning in Asynchronous Domains. Artificial Intelligence 174 (2005)Google Scholar
  9. 9.
    Moussa, H., Gao, T., Yen, I.L., Bastani, F., Jeng, J.J.: Toward effective service composition for real-time SOA-based systems. Service Oriented Computing and Applications 4(1) (2010)Google Scholar
  10. 10.
    Lin, L., Lin, P.: Orchestration in Web Services and Real-Time Communications. IEEE Communications Magazine (July 2007)Google Scholar
  11. 11.
    Kallel, S., Dinkelaker, T., Mezini, M., Charfi, A., Jmaiel, M.: Specifying and Monitoring Temporal Properties in Web services Compositions. In: Seventh IEEE European Conference on Web Services (2009)Google Scholar
  12. 12.
    Stöhr, D., Glesner, S.: Automated Composition of Timed Services by Planning as Model Checking. In: Proceedings of the 4th Central European Workshop on Services and their Composition (2012)Google Scholar
  13. 13.
    Do, M.B., Kambhampati, S.: Sapa: A Domain-Independent Heuristic Metric Temporal Planner. In: Proceedings of European Conference on Planning (2001)Google Scholar
  14. 14.
    Garrido, A., Fox, M., Long, D.: A Temporal Planning System for Durative Actions of PDDL2.1. In: European Conference on AI, vol. 1 (2002)Google Scholar
  15. 15.
    Muscettola, N.: HSTS: Integrating Planning and Scheduling. Intelligent Scheduling (1993)Google Scholar
  16. 16.
    Doherty, P., Kvarnström, J., Heintz, F.: A temporal logic-based planning and execution monitoring framework for unmanned aircraft systems. In: Autonomous Agents and Multi-Agent Systems, vol. 19(3) (2009)Google Scholar
  17. 17.
    Cassez, F., David, A., Fleury, E., Larsen, K.G.: Efficient On-the-fly Algorithms for the Analysis of Timed Games (2005)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Daniel Stöhr
    • 1
  • Sabine Glesner
    • 1
  1. 1.Software Engineering for Embedded SystemsTechnical University of BerlinGermany

Personalised recommendations