From unified modeling language : modeling and analysis of real-time embedded systems component based specifications to communicating sequential processes-object Z specifications

العناوين الأخرى

التحويل من مواصفات لغة النمذجة الموحدة : نمذجة و تحليل أنظمة الزمن الحقيقي الضمنية ذات البنية التكوينية إلى مواصفات العمليات المتسلسلة التواصلية-كائن زي

مقدم أطروحة جامعية

al-Sayih, Khalid Nasir Ahmad

مشرف أطروحة جامعية

Bittaz, Muhammad

الجامعة

جامعة فيلادلفيا

الكلية

كلية تكنولوجيا المعلومات

القسم الأكاديمي

قسم علم الحاسوب

دولة الجامعة

الأردن

الدرجة العلمية

ماجستير

تاريخ الدرجة العلمية

2018

الملخص الإنجليزي

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).

التخصصات الرئيسية

تكنولوجيا المعلومات وعلم الحاسوب

الموضوعات

• لغات البرمجة

عدد الصفحات

58

قائمة المحتويات

• APA
• MLA
• AMA

لغة النص

الإنجليزية

نوع البيانات

رسائل جامعية

رقم السجل

BIM-955499