Verification Validation of Object-Oriented Functional Design using Formal Specification Techniques

摘要

UML is now an ISO standard used for graphically representing software systems. It possesses key advantages such as simplicity, intuitiveness and recently it has been considered as a semi-formal specification notation. However, UML falls short in the latter area because it utilizes loose semantics which leads to ambiguity among its models. In some cases ambiguity can be negligible, however in safety critical systems this may lead to detrimental consequences. One technique to eliminate this ambiguity is to transform UML models into an analyzable representation with the use of formal specification techniques. Prior work has been conducted in formalizing UML class diagram attribute constraints and from that research, the work conducted here follows to demonstrate formalizing the operation signatures of the said classes within the UML class diagram. This effort will look at how UML model verification and validation can be done by analyzing pre- and post-conditions of user-defined functions using Z notation - a formal specification language.