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 136
- Downloads 0
Securing Gateways within Clustered Power Centric Network of Nodes
Knowledge Networks are gaining momentum within cyber world. Knowledge leads to innovation and for this reason organizations focus on research and information gathering in order to gain and improve existing knowledge. Thi...
Improved Cooperation in Underwater Wireless Sensor Networks
The WSNs (Wireless Sensor Networks) lead to great opportunities to explore it scientifically. In this network different numbers of SN (Sensor Nodes) are deployed in a specific area to gather information. The UWSNs (Under...
Flood Management Current State, Challenges and Prospects in Pakistan: A Review
Flooding is globally a major natural hazard. Floods result in property and life loss and poor economic development. Though it is not possible to prevent the occurrence of floods, but their negative impacts could be minim...
Factors Contributing to the Waste Generation in Building Projects of Pakistan
Generation of construction waste is a worldwide issue that concerns not only governments but also the building actors involved in construction industry. For developing countries like Pakistan, rising levels of waste gene...
Optimization by Genetic Algorithm in Wireless Sensor Networks Utilizing Multiple Sinks
WSN (Wireless Sensor Network) comprises of small-sized and constraint-capability SN (Sensor Nodes) which record, send and receive data, sensed to a sink. The network lifetime and energy usability are important challenges...