Translating Activity Diagram from Duration Calculus for Modeling of Real-Time Systems and its Formal Verification using UPPAAL and DiVinE
Journal: Mehran University Research Journal of Engineering and Technology (Vol.35, No. 1)Publication Date: 2016-01-01
Authors : Muhammad Abdul Basit Ur Rahim; Fahim Arif;
Page : 139-154
Keywords : Formal Semantics; Formal Modeling; Real-Time System; Verification; UPPAAL; DiVinE;
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.
Other Latest Articles
- Estimation of Energy Potential from Organic Fractions of Municipal Solid Waste by Using Empirical Models at Hyderabad, Pakistan
- Physical and Psychological Responses in a Data Entry Task
- Solar Thermal Technologies Dynamics and Strategies for Market Creation in Sindh
- Voltage Harmonics Mitigation through Hybrid Active Power Filter
- Factors Contributing to the Waste Generation in Building Projects of Pakistan
Last modified: 2016-01-10 00:25:21