Skip to main content
SpringerLink
Log in

Automated Translation and Analysis of a ToolBus Script for Auctions

  • Conference paper
Fundamentals of Software Engineering (FSEN 2009)

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

Included in the following conference series:

  • 463 Accesses

Abstract

ToolBus allows to connect tools via a software bus. Programming is done using the scripting language Tscript, which is based on the process algebra ACP. In previous work we presented a method for analyzing a Tscript by translating it to the process algebraic language mCRL2, and then applying model checking to verify certain behavioral properties. We have implemented a prototype based on this approach. As a case study, we have applied it on a standard example from the ToolBus distribution, distributed auction, and detected a number of behavioral irregularities in this auction Tscript.

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. Bergstra, J.A., Klint, P.: The ToolBus coordination architecture. In: Hankin, C., Ciancarini, P. (eds.) COORDINATION 1996. LNCS, vol. 1061, pp. 75–88. Springer, Heidelberg (1996)

    Google Scholar 

  2. Bergstra, J.A., Klint, P.: The discrete time ToolBus - a software coordination architecture. Sci. Comput. Program. 31(2-3), 205–229 (1998)

    Article  MATH  Google Scholar 

  3. Bergstra, J.A., Klop, J.W.: Process algebra for synchronous communication. Information and Control 60(1-3), 109–137 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  4. Fokkink, W., Klint, P., Lisser, B., Usenko, Y.S.: Towards formal verification of ToolBus scripts. In: Meseguer, J., Roşu, G. (eds.) AMAST 2008. LNCS, vol. 5140, pp. 160–166. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  5. Groote, J.F., Mathijssen, A.H.J., Reniers, M.A., Usenko, Y.S., van Weerdenburg, M.J.: The formal specification language mCRL2. In: Proc. Methods for Modelling Software Systems. Dagstuhl Seminar Proceedings, vol. 06351 (2007)

    Google Scholar 

  6. Bergstra, J.A., Heering, J., Klint, P.: Module algebra. J. ACM 37(2), 335–372 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  7. Garavel, H., Mateescu, R., Lang, F., Serwe, W.: CADP 2006: A toolbox for the construction and analysis of distributed processes. In: Damm, W., Hermanns, H. (eds.) CAV 2007. LNCS, vol. 4590, pp. 158–163. Springer, Heidelberg (2007)

    Chapter  Google Scholar 

  8. Groote, J.F., Willemse, T.A.C.: Parameterised boolean equation systems. Theor. Comput. Sci. 343(3), 332–369 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  9. Wing, J.M.: Writing Larch interface language specifications. ACM Trans. Program. Lang. Syst. 9(1), 1–24 (1987)

    Article  MATH  MathSciNet  Google Scholar 

  10. Guaspari, D., Marceau, C., Polak, W.: Formal verification of Ada programs. IEEE Trans. Software Eng. 16(9), 1058–1075 (1990)

    Article  Google Scholar 

  11. Zhao, J., Rinard, M.C.: Pipa: A behavioral interface specification language for aspectJ. In: Pezzé, M. (ed.) FASE 2003. LNCS, vol. 2621, pp. 150–165. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  12. Kiczales, G., Hilsdale, E., Hugunin, J., Kersten, M., Palm, J., Griswold, W.G.: An overview of aspectJ. In: Knudsen, J.L. (ed.) ECOOP 2001. LNCS, vol. 2072, pp. 327–353. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  13. Larsson, D., Alexandersson, R.: Formal verification of fault tolerance aspects. In: Supplementary Proceedings of International Symposium on Software Reliability Engineering (ISSRE) Conference, pp. 279–280. IEEE, Los Alamitos (2005)

    Google Scholar 

  14. Hilderink, G.H., Bakkers, A.W.P., Broenink, J.F.: A distributed real-time Java system based on CSP. In: Proc. ISORC 2000, pp. 400–410. IEEE, Los Alamitos (2000)

    Google Scholar 

  15. Orlic, B., Broenink, J.F.: Design Principles of the SystemCSP Software Framework. In: McEwan, A.A., Ifill, W., Welch, P.H. (eds.) CPA 2007, pp. 207–228 (2007)

    Google Scholar 

  16. Hopcroft, P.J., Broadfoot, G.H.: Combining the box structure development method and CSP for software development. Electr. Notes Theor. Comput. Sci. 128(6), 127–144 (2005)

    Article  Google Scholar 

  17. Prowell, S.J., Poore, J.H.: Foundations of sequence-based software specification. IEEE Trans. Software Eng. 29(5), 417–429 (2003)

    Article  Google Scholar 

  18. Broadfoot, G.H.: Asd case notes: Costs and benefits of applying formal methods to industrial control software. In: Fitzgerald, J.S., Hayes, I.J., Tarlecki, A. (eds.) FM 2005. LNCS, vol. 3582, pp. 548–551. Springer, Heidelberg (2005)

    Google Scholar 

  19. Doxsee, S., Gardner, W.B.: Synthesis of C++ software from verifiable CSPm specifications. In: Proc. ECBS 2005, pp. 193–201 (2005)

    Google Scholar 

  20. Beek, B., Man, K.L., Reniers, M., Rooda, K., Schiffelers, R.: Syntax and consistent equation semantics of hybrid χ. J. Log. Algebr. Program. 68(1-2), 129–210 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  21. Braspenning, N.C.W.M., van de Mortel-Fronczak, J.M., Rooda, J.E.: A model-based integration and testing method to reduce system development effort. Electr. Notes Theor. Comput. Sci. 164(4), 13–28 (2006)

    Article  Google Scholar 

  22. Diertens, B.: Simulation and animation of process algebra specifications. Technical Report P9713, University of Amsterdam (1997)

    Google Scholar 

  23. Diertens, B.: Software (re-)engineering with PSF III: An IDE for PSF. Technical Report PRG0708, University of Amsterdam (2007)

    Google Scholar 

  24. van der Brand, M., de Jong, H., Klint, P., Olivier, P.: Efficient annotated terms. Softw., Pract. Exper. 30(3), 259–291 (2000)

    Article  Google Scholar 

  25. Klint, P.: A meta-environment for generating programming environments. ACM TOSEM 2(2), 176–201 (1993)

    Article  Google Scholar 

  26. den van Brand, M.G.J., van Deursen, A., Heering, J., de Jong, H.A., de Jonge, M., Kuipers, T., Klint, P., Moonen, L., Olivier, P.A., Scheerder, J., Vinju, J.J., Visser, E., Visser, J.: The ASF+SDF meta-environment: A component-based language development environment. In: Wilhelm, R. (ed.) CC 2001. LNCS, vol. 2027, pp. 365–370. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  27. Fokkink, W., Ioustinova, N., Kesseler, E., van de Pol, J., Usenko, Y.S., Yushtein, Y.A.: Refinement and verification applied to an in-flight data acquisition unit. In: Brim, L., Jančar, P., Křetínský, M., Kucera, A. (eds.) CONCUR 2002. LNCS, vol. 2421, pp. 1–23. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  28. Blom, S., Ioustinova, N., Sidorova, N.: Timed verification with μCRL. In: Broy, M., Zamulin, A.V. (eds.) PSI 2003. LNCS, vol. 2890, pp. 178–192. Springer, Heidelberg (2004)

    Google Scholar 

  29. Wijs, A.: Achieving discrete relative timing with untimed process algebra. In: ICECCS, pp. 35–46. IEEE, Los Alamitos (2007)

    Google Scholar 

  30. Mateescu, R., Sighireanu, M.: Efficient on-the-fly model-checking for regular alternation-free mu-calculus. Sci. Comput. Program. 46(3), 255–281 (2003)

    Article  MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Software Engineering Cluster, Centrum voor Wiskunde en Informatica, Amsterdam, The Netherlands

    Wan Fokkink, Paul Klint, Bert Lisser & Yaroslav S. Usenko

  2. Theoretical Computer Science Section, Vrije Universiteit Amsterdam, The Netherlands

    Wan Fokkink

  3. Programming Research Group, Universiteit van Amsterdam, The Netherlands

    Paul Klint

  4. INRIA Lille - Nord Europe, Parc Scientifique de la Haute Borne, 40, avenue Halley, Bat.A, Park Plaza, 59650, Villeneuve d’Ascq, France

    Yaroslav S. Usenko

Authors
  1. Wan Fokkink
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Paul Klint
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Bert Lisser
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Yaroslav S. Usenko
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Center for Mathematics and Computer Science (CWI), Science Park 123, 1098 XG, Amsterdam, The Netherlands

    Farhad Arbab

  2. Reykjavik University, School of Computer Science, Kringlan 1, 103, Reykjavik, Iceland

    Marjan Sirjani

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Fokkink, W., Klint, P., Lisser, B., Usenko, Y.S. (2010). Automated Translation and Analysis of a ToolBus Script for Auctions. In: Arbab, F., Sirjani, M. (eds) Fundamentals of Software Engineering. FSEN 2009. Lecture Notes in Computer Science, vol 5961. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-11623-0_18

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-11623-0_18

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-11622-3

  • Online ISBN: 978-3-642-11623-0

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation