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...
| Main Author: | |
|---|---|
| Format: | Thesis |
| Language: | English |
| Published: |
Universiti Malaysia Sarawak, (UNIMAS)
2010
|
| Subjects: | |
| Online Access: | http://ir.unimas.my/id/eprint/12075/ http://ir.unimas.my/id/eprint/12075/4/Anding%20ft.pdf |
| _version_ | 1848837122409103360 |
|---|---|
| author | Anding, Anak Nyuak |
| author_facet | Anding, Anak Nyuak |
| author_sort | Anding, Anak Nyuak |
| building | UNIMAS Institutional Repository |
| collection | Online Access |
| description | 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. |
| first_indexed | 2025-11-15T06:34:38Z |
| format | Thesis |
| id | unimas-12075 |
| institution | Universiti Malaysia Sarawak |
| institution_category | Local University |
| language | English |
| last_indexed | 2025-11-15T06:34:38Z |
| publishDate | 2010 |
| publisher | Universiti Malaysia Sarawak, (UNIMAS) |
| recordtype | eprints |
| repository_type | Digital Repository |
| spelling | unimas-120752025-05-16T03:08:44Z http://ir.unimas.my/id/eprint/12075/ Validate object-oriented models using VDM++ Anding, Anak Nyuak T Technology (General) 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. Universiti Malaysia Sarawak, (UNIMAS) 2010 Thesis NonPeerReviewed text en http://ir.unimas.my/id/eprint/12075/4/Anding%20ft.pdf Anding, Anak Nyuak (2010) Validate object-oriented models using VDM++. Masters thesis, Universiti Malaysia Sarawak, (UNIMAS). |
| spellingShingle | T Technology (General) Anding, Anak Nyuak Validate object-oriented models using VDM++ |
| title | Validate object-oriented models using VDM++ |
| title_full | Validate object-oriented models using VDM++ |
| title_fullStr | Validate object-oriented models using VDM++ |
| title_full_unstemmed | Validate object-oriented models using VDM++ |
| title_short | Validate object-oriented models using VDM++ |
| title_sort | validate object-oriented models using vdm++ |
| topic | T Technology (General) |
| url | http://ir.unimas.my/id/eprint/12075/ http://ir.unimas.my/id/eprint/12075/4/Anding%20ft.pdf |