Comparison of ZOOM with formal methodologies

 

Comparison of ZOOM with formal methodologies

Abstract

As our reliance on the information technology is growing rapidly, software systems are becoming more complex and critical to modern life in many ways such as transportation, finance, manufacture, defense, and health control. However, not every system using current software development technologies is perfect and correct. With traditional system development process, software systems do not always match the real needs and there are always frustrating defects. System failures may cause serious problems of safety and money. To prevent the failures of software systems and increase software reliability, formal methods are the ways to make the systems better.

Formal methods include formal specification that gives a precise definition of the problem, formal development that ensures the implementation conforms to the specification, and automation that provides semi-automatic synthesis of implementations from formal specifications. It helps developers fully understand what they are doing when creating software. Formal methods are practical, beneficial, and cost-effective, but short of supporting tools and experienced developers.

ZOOM stands for Z-based Object-Oriented Modeling notation that is based on the most popular formal methods notation Z. It can be use as the formal foundation for supporting Model-Driven Development (MDD). The ZOOM project contains three integrated parts: Structural Model, Behavior Model, User interface Model, and an Event-Driven Framework. Currently the supporting tools in development phase are:

  • Basic Language Supporting Tools: Parser, Type Checker, UML Mapping Tools and Model Editor.
  • Model Validation Tools: Interpreter, Animator.
  • Transformation Tools: Code Generator.
  • Analytical Tools: Automated Theorem Prover (ATP), Unit Test Generator.

    OCL stands for Object Constraint Language. It is a textual, formal specification language that allows the compact notation of precise, side-effect-free constraints on instances of UML models. OCL specifies object behavior, guidelines for invariants on object fields or state, and guards and conditions on object methods in a precise way using the concepts of set theory and logic. OCL is designed by contract that is more like formal Z schema of formal methods.

    This research will be focused on the case studies of ZOOM language with supporting tools, and followed by the comparison with other formal modeling tools using OCL, Z, or other technologies.

    Project Description

    The ZOOM project is still in the development phase and most supporting tools are partially done. This research will be based on the up-to-date technologies and supporting tools of ZOOM to accomplish the following aspects:
    1. Case studies: use the ZOOM notation and supporting tools to do the following case studies:
      • Address book: Use ZOOM to build structural model, behavior model, and user interface model.
      • Academic model: Use ZOOM to build structural model.
      • Railway control system: Use ZOOM to build behavior model.
      • Membership management system: Use ZOOM to build user interface model.
    2. The comparison of syntax between ZOOM and OCL in following aspects:
      • Language scope and capability
      • Ease of use from developers’ view
      • Level of abstraction
    3. The comparison of toolkit between ZOOM and OCL.

    Current Status

    Initial Presentation

    Plan and Target Dates

    • Phase 1: Proposal
      • Milestone 1: Technologies and Tools Review (August 2003)
      • Milestone 2: Research Proposal (September 2003)
      • Milestone 3: Research Web page (September 2003)
      • Milestone 4: Initial Presentation (October 2003)

    • Phase 2: Case studies of ZOOM
      • Milestone 1: Build ZOOM structure model of Academic Model (October 2003)
      • Milestone 2: Build ZOOM behavior model of Railway control system (October 2003)
      • Milestone 3: Build ZOOM user interface model of Membership management system (October 2003)
      • Milestone 4: Build Address book application with ZOOM framework (October 2003)

    • Phase 3: Comparison and Integration
      • Milestone 1: Comparison with other formal toolkits (November 2003)
      • Milestone 2: Work on final paper (November 2003)
      • Milestone 3: Final presentation (November 2003)

    • Completion: November 2003

    Documents

    References

    1. Hongming Liu, Lizhang Qin, Chris Jones, Xiaoping Jia, An Formal Foundation Supporting MDD -- ZOOM Approach, October 2003.
    2. Jonathan Jacky, The way of Z, Cambridge University Press, 1997
    3. Katone, Verification and Validation.
    4. Object Constraint Language Specification, OMG, 2003
    • 1