Translating Activity Diagram from Duration Calculus for Modeling of Real-Time Systems and its Formal Verification using UPPAAL and DiVinE
Journal Title: Mehran University Research Journal of Engineering and Technology - Year 2016, Vol 35, Issue 1
Abstract
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.
Authors and Affiliations
Muhammad Abdil Basit Ur Rahim, Fahim Arif
Keywords
Related Articles
- EP ID EP191399
- DOI -
- Views 135
- Downloads 0
Problem of Traffic Congestion and Correlation Analysis of Driving behaviors in Qasimabad, Hyderabad
In this study, we explore the problem of traffic congestion, its effects and related issues for Qasimabad, Hyderabad, Pakistan. The study is based on survey conducted at different sites of Qasimabad. The data was collect...
Power Flow Analysis of the Enhanced Proposed 330kV Transmission Network of the Nigeria Grid
The Nigeria’s power sector transmission infrastructure continues to be challenged as it still remains the weak link in the electricity supply chain. The Nigerian Federal Government on its Roadmap for power sector reform...
Just-in-Time Compilation-Inspired Methodology for Parallelization of Compute Intensive Java Code
Compute intensive programs generally consume significant fraction of execution time in a small amount of repetitive code. Such repetitive code is commonly known as hotspot code. We observed that compute intensive hotspot...
Matched Filter Based Spectrum Sensing Technique for 4G Cellular Network
Modern and fast developments of wireless technologies have directed to a great demand for resources. It can be seen in the study that the range of existing spectrum is not used effectively, therefore the frequency band s...
Effective Compression of Center Symmetric Local Binary Pattern
In this paper, we propose simple and effective compression of CSLBP (Center Symmetric Local Binary Pattern) descriptors, which is a textured based operator and mostly used as key point descriptor. With default parameters...