Software Engineering Research Project
Description
Updated on 09/28/2003
Contact Info
Name: Hsiu-Chien Jing
E-mail: [email protected]
Webpage: http://www.geocities.com/jinghsiuchien/SE690.htm
Project Type
- SE Research Seminar (SE690 only)
Project Title
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:
- 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.
- The comparison of syntax between ZOOM and OCL in following aspects:
- Language scope and capability
- Ease of use from developers’ view
- Level of abstraction
- 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
- Hongming Liu, Lizhang Qin, Chris Jones, Xiaoping Jia, An Formal Foundation Supporting MDD -- ZOOM Approach, October 2003.
- Jonathan Jacky, The way of Z, Cambridge University Press, 1997
- Katone, Verification and Validation.
- Object Constraint Language Specification, OMG, 2003