Validate object-oriented models using VDM++
The goal of this thesis is to generate Formal Method (FM) specifications using the Unified Modeling Language (UML), class diagram models. In this context, we use the Vienna Development Method for modeling object-oriented models (VDM++) as a formal specification language. We studied the syntax and se...
Saved in:
Main Author: | |
---|---|
Format: | Thesis |
Language: | English |
Published: |
2010
|
Subjects: | |
Online Access: | http://ir.unimas.my/id/eprint/12075/3/Anding%20Anak%20Nyuak%20ft.pdf |
Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
Summary: | The goal of this thesis is to generate Formal Method (FM) specifications using the Unified Modeling Language (UML), class diagram models. In this context, we use the Vienna Development Method for modeling object-oriented models (VDM++) as a formal specification language. We studied the syntax and semantic of UML and VDM++ models and then defined the mapping rules that were used to transform UML models into VDM++ specifications. To achieve this purpose, we present a framework of the prototype that,
automatically generates UML models into VDM++ specifications. .lrhe prototype derives UML properties of a class diagram and uses the translation rules to construct VDM++ class, types, values, instance variables and operation signatures. We proposed a rule-based to construct Set and Sequence in VDM++ based on Multiplicity and Ordered/Unordered properties of UML model. We also developed an interactive interface to construct composite data type to model structured data such as record. A transformed model from UML into VDM++ specification then validated and checked using VDMTool Lite vS.l. |
---|