Skip to main content
SpringerLink
Log in

Temporal Specifications for Services with Unboundedly Many Passive Clients

  • Conference paper
Distributed Computing and Networking (ICDCN 2011)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 6522))

Included in the following conference series:

  • 750 Accesses

Abstract

We consider a client-server system in which unbounded, finite but unknown, number of clients request for service from the server. The system is passive as there is no further interaction between send-request and receive-response. We give an automata based model for such systems and a temporal logic to frame specifications. We show that the satisfiability and model checking problems for the logic are decidable.

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 39.99
Price excludes VAT (USA)
  • Available as 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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Berardi, D., Calvanese, D., De Giacomo, G., Lenzerini, M., Mecella, M.: Automatic composition of E-services that export their behavior. In: Orlowska, M.E., Weerawarana, S., Papazoglou, M.P., Yang, J. (eds.) ICSOC 2003. LNCS, vol. 2910, pp. 43–58. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  2. Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A., Winkowski, J. (eds.) CONCUR 1997. LNCS, vol. 1243, pp. 135–150. Springer, Heidelberg (1997)

    Chapter  Google Scholar 

  3. Bultan, T., Fu, X., Hull, R., Su, J.: Conversation specification: a new approach to design and analysis of e-service composition. In: WWW, pp. 403–410 (2003)

    Google Scholar 

  4. Burstein, M.H., Hobbs, J.R., Lassila, O., Martin, D.L., McDermott, D.V., McIlraith, S.A., Narayanan, S., Paolucci, M., Payne, T.R., Sycara, K.P.: Daml-s: Web service description for the semantic web. In: Horrocks, I., Hendler, J. (eds.) ISWC 2002. LNCS, vol. 2342, pp. 348–363. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  5. Clarke, E.M., Grumberg, O., Peled, D.: Model Checking. MIT Press, Cambridge (2000)

    Google Scholar 

  6. Christophides, V., Hull, R., Karvounarakis, G., Kumar, A., Tong, G., Xiong, M.: Beyond discrete E-services: Composing session-oriented services in telecommunications. In: Casati, F., Georgakopoulos, D., Shan, M.-C. (eds.) TES 2001. LNCS, vol. 2193, pp. 58–73. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  7. Deutsch, A., Sui, L., Vianu, V., Zhou, D.: Verification of communicating data-driven web services. In: PODS, pp. 90–99 (2006)

    Google Scholar 

  8. Fu, X., Bultan, T., Su, J.: Conversation protocols: a formalism for specification and verification of reactive electronic services. Theor. Comput. Sci. 328(1-2), 19–37 (2004)

    Article  MathSciNet  MATH  Google Scholar 

  9. Florescu, D., Grünhagen, A., Kossmann, D.: Xl: an xml programming language for web service specification and composition. In: WWW, pp. 65–76 (2002)

    Google Scholar 

  10. Gabbay, D.M., Hodkinson, I.M., Reynolds, M.A.: Temporal Logic. Part 1. Clarendon Press (1994)

    Google Scholar 

  11. Henriksen, J.G., Jensen, J.L., Jørgensen, M.E., Klarlund, N., Paige, R., Rauhe, T., Sandholm, A.: Mona: Monadic second-order logic in practice. In: Brinksma, E., Steffen, B., Cleaveland, W.R., Larsen, K.G., Margaria, T. (eds.) TACAS 1995. LNCS, vol. 1019, pp. 89–110. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  12. Hodkinson, I.M.: Monodic packed fragment with equality is decidable. Studia Logica 72(2), 185–197 (2002)

    Article  MathSciNet  MATH  Google Scholar 

  13. Holzmann, G.J.: The model checker spin. IEEE Trans. Software Eng. 23(5), 279–295 (1997)

    Article  Google Scholar 

  14. Hodkinson, I.M., Wolter, F., Zakharyaschev, M.: Decidable fragment of first-order temporal logics. Ann. Pure Appl. Logic 106(1-3), 85–134 (2000)

    Article  MathSciNet  MATH  Google Scholar 

  15. Hodkinson, I., Wolter, F., Zakharyaschev, M.: Monodic fragments of first-order temporal logics: 2000-2001 A.D. In: Nieuwenhuis, R., Voronkov, A. (eds.) LPAR 2001. LNCS (LNAI), vol. 2250, pp. 1–23. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  16. Hodkinson, I.M., Wolter, F., Zakharyaschev, M.: Decidable and undecidable fragments of first-order branching temporal logics. In: LICS, pp. 393–402 (2002)

    Google Scholar 

  17. Klarlund, N., Møller, A., Schwartzbach, M.I.: Mona implementation secrets. In: Yu, S., Păun, A. (eds.) CIAA 2000. LNCS, vol. 2088, pp. 182–194. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  18. Narayanan, S., McIlraith, S.A.: Simulation, verification and automated composition of web services. In: WWW, pp. 77–88 (2002)

    Google Scholar 

  19. Ruys, T.C., Holzmann, G.J.: Advanced SPIN tutorial. In: Graf, S., Mounier, L. (eds.) SPIN 2004. LNCS, vol. 2989, pp. 304–305. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  20. IBM Web Services Business Process Execution Language (WSBPEL) TC. Web services business process execution language version 1.1. Technical report (2003), http://www.ibm.com/developerworks/library/ws-bpel

  21. Vardi, M.Y., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: LICS, pp. 332–344 (1986)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. The Institute of Mathematical Sciences, C.I.T. Campus, Chennai, 600 113, India

    Shamimuddin Sheerazuddin

Authors
  1. Shamimuddin Sheerazuddin
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Microsoft Research Silicon Valley, 1065 La Avenida – bldg. 6, 94043, Mountain View, CA, USA

    Marcos K. Aguilera

  2. School of Computing, National University of Singapore, COM2-04-25, 15 Computing Drive, 117418, Republic of Singapore

    Haifeng Yu

  3. 458 Coordinated Science Laboratory, University of Illinois at Urbana-Champaign, MC-228, 1308 West Main Street, 61801, Urbana, IL, USA

    Nitin H. Vaidya

  4. Alcatel-Lucent Technologies, Manyata Technology Park, Nagawara, 560045, Bangalore, India

    Vikram Srinivasan

  5. ECE Department, Duke University, 130 Hudson Hall, Box 90291, 27708, Durham, NC, USA

    Romit Roy Choudhury

Rights and permissions

Reprints and permissions

Copyright information

© 2011 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Sheerazuddin, S. (2011). Temporal Specifications for Services with Unboundedly Many Passive Clients. In: Aguilera, M.K., Yu, H., Vaidya, N.H., Srinivasan, V., Choudhury, R.R. (eds) Distributed Computing and Networking. ICDCN 2011. Lecture Notes in Computer Science, vol 6522. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-17679-1_16

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-17679-1_16

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-17678-4

  • Online ISBN: 978-3-642-17679-1

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation