دورية أكاديمية
Translating Activity Diagram from Duration Calculus for Modeling of Real-Time Systems and its Formal Verification using UPPAAL and DiVinE
| العنوان: | Translating Activity Diagram from Duration Calculus for Modeling of Real-Time Systems and its Formal Verification using UPPAAL and DiVinE |
|---|---|
| المؤلفون: | Muhammad Abdul Basit Ur Rehman, Fahim Arif |
| المصدر: | Mehran University Research Journal of Engineering and Technology, Vol 35, Iss 1, Pp 139-154 (2016) |
| بيانات النشر: | Mehran University of Engineering and Technology, 2016. |
| سنة النشر: | 2016 |
| المجموعة: | LCC:Technology LCC:Engineering (General). Civil engineering (General) LCC:Science |
| مصطلحات موضوعية: | Formal Semantics, Formal Modeling, Real-Time System, Verification, UPPAAL, DiVinE, Technology, Engineering (General). Civil engineering (General), TA1-2040, Science |
| الوصف: | The RTS (Real-Time Systems) are widely used in industry, home appliances, life saving systems, aircrafts, and automatic weapons. These systems need more accuracy, safety, and reliability. An accurate graphical modeling and verification of such systems is really challenging. The formal methods made it possible to model such systems with more accuracy. In this paper, we envision a strategy to overcome the inadequacy of SysML (System Modeling Language) for modeling and verification of RTS, and illustrate the framework by applying it on a case study of fuel filling machine. We have defined DC (Duration Calculus) implementaion based formal semantics to specify the functionality of RTS. The activity diagram in then generated from these semantics. Finally, the graphical model is verified using UPPAAL and DiVinE model checkers for validation of timed and untimed properties with accelerated verification speed. Our results suggest the use of methodology for modeling and verification of large scale real-time systems with reduced verification cost. |
| نوع الوثيقة: | article |
| وصف الملف: | electronic resource |
| اللغة: | English |
| تدمد: | 0254-7821 2413-7219 |
| العلاقة: | http://publications.muet.edu.pk/research_papers/pdf/pdf1230.pdfTest; https://doaj.org/toc/0254-7821Test; https://doaj.org/toc/2413-7219Test |
| الوصول الحر: | https://doaj.org/article/594cc481fbec4bb6a16d9012b5103598Test |
| رقم الانضمام: | edsdoj.594cc481fbec4bb6a16d9012b5103598 |
| قاعدة البيانات: | Directory of Open Access Journals |
| تدمد: | 02547821 24137219 |
|---|