From unified modeling language : modeling and analysis of real-time embedded systems component based specifications to communicating sequential processes-object Z specifications
Other Title(s)
التحويل من مواصفات لغة النمذجة الموحدة : نمذجة و تحليل أنظمة الزمن الحقيقي الضمنية ذات البنية التكوينية إلى مواصفات العمليات المتسلسلة التواصلية-كائن زي
Dissertant
Thesis advisor
University
Philadelphia University
Faculty
Faculty of Information Technology
Department
Department of Computer Science
University Country
Jordan
Degree
Master
Degree Date
2018
English Abstract
UML is a language designed for general purpose modelling.
It has profiles that provide generic extension to customize the models for specific languages and domains.
MARTE is a UML profile used for modelling Real-time and embedded systems.
It has been used to facilitate such systems, also has been utilized to handle intra-concurrency feature that is presented by its component RtUnit (Real-time Unit); is similar to the active object, which may be seen as an autonomous execution resource, able to handle different messages at the same time.
However, MARTE does not have the ability to formally verify some properties of the modelled system such as deadlock and liveness.
Therefore, this research work proposes the transformation of UML/MARTE models into the CSPOZ; a formal specification language that combines the Object-Z specification language with process algebra CSP, to solve the problem of formal verification issues.
The transformation between UML/MARTE and CSP-OZ will be straightforward, since both of the frameworks are sharing the same core abstraction.
This thesis work will contribute in twofold.
Firstly, to best of our knowledge this work is the first whose transform UML/MARTE model (RtUnit) to CSP-OZ specification.
Secondly, defining the transformation rules from UML/MARTE to CSP-OZ specification.
This transformation represents the first step of solving MARTE problem in formal verification issues.
As a result, this thesis work presents eight different rules for transforming UML/MARTE component (RtUnit) to CSP-OZ specification, these rules have been applied on the case study (Cruise Control System).
Main Subjects
Information Technology and Computer Science
Topics
No. of Pages
58
Table of Contents
Table of contents.
Abstract.
Abstract in Arabic.
Chapter One : Introduction
Chapter Two : Background.
Chapter Three : Literature review.
Chapter Four : Contribution and case study.
Chapter Five : Evaluation.
Chapter Six : Conclusion and Future Work.
References.
American Psychological Association (APA)
al-Sayih, Khalid Nasir Ahmad. (2018). From unified modeling language : modeling and analysis of real-time embedded systems component based specifications to communicating sequential processes-object Z specifications. (Master's theses Theses and Dissertations Master). Philadelphia University, Jordan
https://search.emarefa.net/detail/BIM-955499
Modern Language Association (MLA)
al-Sayih, Khalid Nasir Ahmad. From unified modeling language : modeling and analysis of real-time embedded systems component based specifications to communicating sequential processes-object Z specifications. (Master's theses Theses and Dissertations Master). Philadelphia University. (2018).
https://search.emarefa.net/detail/BIM-955499
American Medical Association (AMA)
al-Sayih, Khalid Nasir Ahmad. (2018). From unified modeling language : modeling and analysis of real-time embedded systems component based specifications to communicating sequential processes-object Z specifications. (Master's theses Theses and Dissertations Master). Philadelphia University, Jordan
https://search.emarefa.net/detail/BIM-955499
Language
English
Data Type
Arab Theses
Record ID
BIM-955499
