[go: up one dir, main page]
More Web Proxy on the site http://driver.im/ Skip to main content
Springer Nature Link
Log in

State-based versus event-based specifications for information systems: a comparison of B and eb3

  • Special section
  • Published:
Software & Systems Modeling Aims and scope Submit manuscript

Abstract

This paper compares two formal methods, B and eb3, for specifying information systems. These two methods are chosen as examples of the state-based paradigm and the event-based paradigm, respectively. The paper considers four viewpoints: functional behavior expression, validation, verification, and evolution. Issues in expressing event ordering constraints, data integrity constraints, and modularity are thereby considered. A simple case study is used to illustrate the comparison, namely, a library management system. Two equivalent specifications are presented using each method. The paper concludes that B and eb3 are complementary. The former is better at expressing complex ordering and static data integrity constraints, whereas the latter provides a simpler, modular, explicit representation of dynamic constraints that are closer to the user’s point of view, while providing loosely coupled definitions of data attributes. The generality of these results from the state-based paradigm and the event-based paradigm perspective are discussed.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
£29.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price includes VAT (United Kingdom)

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Abrial J-R (1996) The B-Book. Cambridge University Press, Cambridge, UK

  2. Abrial J-R (1996) Extending B without Changing it. In: Habrias H (ed) First Conference on the B Method, pp 169–190, November 1996

  3. Abrial J-R, Mussat L (1998) Introducing Dynamic Constraints in B. In: Bert D (ed) Second International B Conference, Lecture Notes in Computer Science, vol 1393. Springer-Verlag, pp 83–128, April 1998

  4. Behm P, Benoit P, Faivre A, Meynadier JM (1999) Météor: A Successful Application of B in a Large Project. In: FM99: World Congress on Formal Methods, Toulouse, France, Lecture Notes in Computer Science, vol 1708. Springer-Verlag, pp 369–387, September 1999

  5. Boehm BW (1984) Verifying and Validating Software Requirements and Design Specifications. IEEE Software 1(1):75–88, January 1984

    Article  Google Scholar 

  6. Boerger E, Staerk R (2003) Abstract State Machines: A Method for High-Level System Design and Analysis. Springer-Verlag, ISBN 3-540-00702-4

    Google Scholar 

  7. Bolognesi T, Brinksma E (1987) Introduction to the ISO Specification Language Lotos. Computer Networks and ISDN Systems 14(1):25–59

    Article  Google Scholar 

  8. Butler MJ, Waldén M (1996) Distributed System Development in B. In: Habrias H (ed) First Conference on the B Method, November 1996

  9. Butler M (2000) csp2B: A Practical Approach to Combining CSP and B. Formal Aspects of Computing 12(4):182–198

    Article  Google Scholar 

  10. CLEARSY System Engineering: Aix-en-Provence, France, http://www.clearsy.com/

  11. Darlot C (2002) Reformulation et vérification de propriétés temporelles dans le cadre du raffinement de systèmes d’événements. Ph.D. thesis, Université de Franche-Comté, France

  12. Elmasri R, Navathe SB (2004) Fundamentals of Database Systems. 4th edition, Addison-Wesley

  13. Emerson EA, Kahlon V (2000) Reducing model checking of the many to the few. In: Proceedings of CADE’2000, Lecture Notes in Computer Science, vol 1831. Springer-Verlag, pp 236–354

  14. Evans N, Treharne H, Laleau R, Frappier M (2004) How to Verify Dynamic Properties of Information Systems. In: Cuellar JR, Liu Z (eds) 2nd IEEE International Conference on Software Engineering and Formal Methods, Beijing, China, 26–30 September 2004. IEEE Computer Society Press, pp 416–425.

  15. Fischer C (2000) Combination and Implementation of Processes and Data: from CSP-OZ to Java. PhD thesis, University of Oldenburg

    Google Scholar 

  16. Formal Systems (Europe) Ltd. (1997) Failures-Divergences Refinement: FDR2 User Manual. http://www.formal.demon.co.uk

  17. Fraikin B, Frappier M (2002) eb3PAI: an interpreter for the eb3 specification language. In: FM-TOOLS 2002, The 5th Workshop on Tools for System Design and Verification, Reisensburg Castle, Günzburg, Germany, 15–17 July 2002

  18. Fraikin B, Frappier M (2002) Optimizing memory space in the eb3 process algebra interpreter. In: ICCSSEA 2002, Software and Systemes Engineering and their Applications, vol I, Session 4

  19. Frappier M, Laleau R (2003) Proving Event Ordering Properties for Information Systems. In: Zb 2003: Formal Specification and Development in Z and B, Turku, Finland, 4–6 June 2003, Lecture Notes in Computer Science, vol 2651. Springer-Verlag, pp 421–436

  20. Frappier M, St-Denis R (2003) eb3: an Entity-Based Black-Box Specification Method for Information Systems. Software and System Modeling 2(2):134–149, July 2003

    Article  Google Scholar 

  21. Gervais F (2004) EB4: Vers une méthode combinée de spécification formelle des systèmes d’information. Examen de spécialité, Doctorat Informatique, Université de Sherbrooke, June 2004

  22. Hoare CAR (1985) Communicating Sequential Processes. Prentice Hall, Englewood Cliffs

  23. INRIA Rhône-Alpes: CADP (Caesar/Aldebaran Development Package), http://www.inrialpes.fr/vasy/cadp/

  24. Jarke M, Mylopoulos J, Schmidt JW, Vassiliou Y (1992) DAIDA: An Environment for Evolving Information Systems. ACM Transactions on Information Systems 10(1):1–50, January 1992

    Article  Google Scholar 

  25. Laleau R Mammar A (2000) An Overview of a Method and its Support Tool for Generating B Specifications from UML Notations. In: ASE: 15th IEEE Conference on Automated Software Engineering, Grenoble, France, September 2000, IEEE Computer Society Press

  26. Laleau R, Mammar A (2000) A Generic Process to Refine a B Specification into a Relational Database Implementation. In: ZB2000: Formal Specification and Development in Z and B, Lecture Notes in Computer Science, vol 1878, Springer-Verlag, York

  27. Laleau R (2002) Conception et développement formels d’applications bases de données. Habilitation Thesis, CEDRIC Laboratory, Évry, France. Available at http://cedric.cnam.fr/PUBLIS/RC424.ps.gz

  28. Mammar A (2002) Un environnement formel pour le développement d’applications bases de données. Ph.D. thesis, CEDRIC Laboratory, CNAM, Evry, France, November 2002. Available at http://cedric.cnam.fr/PUBLIS/RC392.ps.gz

  29. Manna M, Pnueli A (1992) The temporal logic of reactive and concurrent systems. Springer-Verlag

  30. Meyer E, Souquières J (1999) A Systematic approach to Transform OMT Diagrams to a B specification. In: Wing JM, Woodcook J, Davies J (eds) Formal Methods (FM’99), September 1999, Lecture Notes in Computer Science, vol 1708(1), Springer-Verlag, pp 875–895

  31. Mills HD, Linger R.C., Hevner AR (1986) Principles of Information Systems Analysis and Design. Academic Press, Orlando, FL

  32. Milner R (1989) Communication and Concurrency. Prentice Hall, Englewood Cliffs

  33. Pnueli A (1981) The temporal semantics of concurrent programs. Theoretical Computer Science 13:45–60

    Article  MathSciNet  Google Scholar 

  34. Snook C, Butler M (2004) UML-B: Formal modelling and design aided by UML. Technical Report, Department of Electronics and Computer Science, University of Southampton, United Kingdom. http://www.ecs.soton.ac.uk/people/mjb/

  35. Treharne H, Schneider S (2000) How to drive a B machine. In: Bowen JP, Dunne S, Galloway A, King S (eds) ZB2000: Formal Specification and Development in Z and B, LNCS vol 1878, Springer-Verlag, pp 188–208

  36. Vissers CA, Scollo G, van Sinderen M (1988) Architecture and specification style in formal descriptions of distributed systems. In: Aggarwal S, Sabnani K (eds) Protocol Specification, Testing and Verification, VIII, North-Holland, Amsterdam, pp 189–204

  37. Woodcock JCP, Cavalcanti ALC (2002) The Semantics of Circus. In: ZB 2002: Formal Specification and Development in Z and B, Grenoble, France, 2002, LNCS vol 2272. Springer-Verlag

Download references

Author information

Authors and Affiliations

  1. GRIL, Département d’informatique, Université de Sherbrooke, Sherbrooke, Québec, Canada, J1K 2R1

    Benoît Fraikin & Marc Frappier

  2. Laboratoire LACL, IUT de Fontainebleau – Département Informatique, Université Paris 12, Route Hurtault, 77300, Fontainebleau, France

    Régine Laleau

Authors
  1. Benoît Fraikin
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Marc Frappier
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Régine Laleau
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Benoît Fraikin.

Rights and permissions

Reprints and permissions

About this article

Cite this article

Fraikin, B., Frappier, M. & Laleau, R. State-based versus event-based specifications for information systems: a comparison of B and eb3. Softw Syst Model 4, 236–257 (2005). https://doi.org/10.1007/s10270-005-0083-4

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10270-005-0083-4

Keywords

Search

Navigation