Welcome To UTPedia

We would like to introduce you, the new knowledge repository product called UTPedia. The UTP Electronic and Digital Intellectual Asset. It stores digitized version of thesis, dissertation, final year project reports and past year examination questions.

Browse content of UTPedia using Year, Subject, Department and Author and Search for required document using Searching facilities included in UTPedia. UTPedia with full text are accessible for all registered users, whereas only the physical information and metadata can be retrieved by public users. UTPedia collaborating and connecting peoples with university’s intellectual works from anywhere.

Disclaimer - Universiti Teknologi PETRONAS shall not be liable for any loss or damage caused by the usage of any information obtained from this web site.Best viewed using Mozilla Firefox 3 or IE 7 with resolution 1024 x 768.

Transforming OCL to PVS: Using Theorem Proving Support for Analysing Model Constraints

Ab. Rahim, Lukman (2007) Transforming OCL to PVS: Using Theorem Proving Support for Analysing Model Constraints. Masters thesis, Universiti Teknologi Petronas.

[img] PDF
Download (6Mb)


The Unified Modelling Language (UML) is a de facto standard language for describing software systems. UML models are often supplemented with Object Constraint Language (OCL) constraints, to capture detailed properties of components and systems. Sophisticated tools exist for analysing UML models, e.g., to check that well-formedness rules have been satisfied. As well, tools are becoming available to analyse and reason about OCL constraints. Previous work has been done on analysing OCL constraints by translating them to formal languages and then analysing the translated constraints with tools such as theorem provers. This project contributes a transformation from OCL to the specification language of the Prototype Verification System (PVS). PVS can be used to analyse and reason about translated OCL constraints. A particular novelty of this project is that it carries out the transformation of OCL to PVS by using model transformation, as exemplified by the OMG's Model-Driven Architecture. The project implements and automates model transformations from OCL to PVS using the Epsilon Transformation Language (ETL) and tests the results using the Epsilon Comparison Language (ECL ).

Item Type: Thesis (Masters)
Academic Subject : Academic Department - Information Communication Technology
Subject: T Technology > T Technology (General)
Divisions: Sciences and Information Technology > Computer and Information Sciences
Depositing User: Users 2053 not found.
Date Deposited: 30 Sep 2013 16:55
Last Modified: 25 Jan 2017 09:45
URI: http://utpedia.utp.edu.my/id/eprint/7750

Actions (login required)

View Item View Item

Document Downloads

More statistics for this item...