Some Guidelines for Formal Development of Web-Based Applications in B-Method

  • Abdolbaghi Rezazadeh
  • Michael Butler
Part of the Lecture Notes in Computer Science book series (LNCS, volume 3455)


Web-based applications are the most common form of distributed systems that have gained a lot of attention in the past ten years. Today many of us are relying on scores of mission-critical Web-based systems in different areas such as banking, finance, e-commerce and government. The development process of these systems needs a sound methodology, which ensures quality, consistency and integrity. Formal Methods provide systematic and quantifiable approaches to create coherent systems. Despite this there has been limited work on the formal modelling of Web-based applications. In this paper our aim is to provide researchers with some guidelines based on results from ongoing work to model a Web-based system using the B-Method. Session and state management, developing formal models for complex data types, abstraction of distributed database systems and formal representation of communication links between different components of a web-based system are the main issues that we have examined.


Abstract Model Server Side Formal Development Client Side Travel Agency 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Murugesan, S., Desphande, Y. (eds.): Web Engineering. LNCS, vol. 2016, p. 3. Springer, Heidelberg (2001)zbMATHCrossRefGoogle Scholar
  2. 2.
    Murugesan, S., et al.: Web Engineering: A New Discipline for Development of Web-based Systems. In: Lomas, M. (ed.) Security Protocols 1996. LNCS, vol. 1189. Springer, Heidelberg (1997)Google Scholar
  3. 3.
    Deshpande, Y., et al.: Web Engineering: Beyond CS, IS and SE. In: Proceedings of the First ICSE Workshop on Web Engineering, Los Angeles, pp. 171–176 (1999)Google Scholar
  4. 4.
    Abrial, J.R.: The B book - Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)zbMATHCrossRefGoogle Scholar
  5. 5.
    Sekerinski, E., Sere, K. (eds.): Program Development by Refinement Case Studies Using the B Method. Springer, Heidelberg (1998)Google Scholar
  6. 6.
    Luigia, P., et al.: A Methodology for Integrating of Formal Methods in a Healthcare Case Study. Technical Report 436 TUCS (2001)Google Scholar
  7. 7.
    Butler, M., Waldén, M.: Distributed system development in B. In: Proceedings of the 1st Conference on the B Method, Nantes, France, pp. 155–168 (1996)Google Scholar
  8. 8.
    Abrial, J.-R., Cansell, D.: Click’n’Prove- Interactive Proofs Within Set Theory, Version 23 (2003),
  9. 9.
    (Atelier B Web Page),
  10. 10.
    (B4free Web Page),
  11. 11.
    Abrial, J.-R.: Extending B without changing it (for developing Distributed Systems). In: Abrias, H. (ed.) Proceedings of the 1st Conference on the B Method, pp. 169–191 (1996)Google Scholar
  12. 12.
    Abrial, J.-R., Mussat, L.: Introducing Dynamic Constraints in B. In: Bert, D. (ed.) B 1998. LNCS, vol. 1393, pp. 83–128. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  13. 13.
    Waldén, M., Sere, K.: Reasoning About Action Systems Using the B-Method. Formal Methods in Systems Design 13, 5–35 (1998)CrossRefGoogle Scholar
  14. 14.
    Back, R., Sere, K.: Superposition Refinement of Reactive Systems. Formal Aspects of Computing 8, 324–346 (1996)zbMATHCrossRefGoogle Scholar
  15. 15.
    Ferreira, C., Butler, M.: Using B Refinement to Analyse Compensating Business Processes. In: Bert, D., Bowen, J.P., King, S. (eds.) ZB 2003. LNCS, vol. 2651, pp. 477–496. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  16. 16.
    Butler, M.J.: Stepwise Refinement of Communicating Systems. Science of Computer Programming 27, 139–173 (1996)zbMATHCrossRefMathSciNetGoogle Scholar
  17. 17.
    Rezazadeh, A., Butler, M.: Event-Based Modelling and Refinement of Distributed Monitoring and Control Systems. In: Refinement of Critical Systems (RCS 2003), Turku (2003)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2005

Authors and Affiliations

  • Abdolbaghi Rezazadeh
    • 1
  • Michael Butler
    • 1
  1. 1.School of Electronics and Computer ScienceUniversity of SouthamptonHighfield, SouthamptonUnited Kingdom

Personalised recommendations