Translating Activity Diagram from Duration Calculus for Modeling of Real-Time Systems and its Formal Verification using UPPAAL and 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.

Authors and Affiliations

Muhammad Abdil Basit Ur Rahim, Fahim Arif

Keywords

Related Articles

Plasmonic Effect of Gold Nanoparticles Surrounded by Multidielectric Matrices

Plasmonic materials are the artificially manufactured materials (metamaterials) typically composed of nanostructure noble metals which give the unique optical properties superior to naturally occurring materials. Such pl...

Design and Performance of Broadband Dual Layer Circular Polarizer Based on Frequency Selective Surface for X-Band Applications

A dual-layer circular polarizer based on FSS (Frequency Selective Surface) composed of two periodic strips in xoy plane. The transmission characteristic of present structure is comprehensively investigated that convert l...

A Novel Hybrid Moth Flame Optimization with Sequential Quadratic Programming Algorithm for Solving Economic Load Dispatch Problem

The insufficiency of energy resources, increased cost of generation and rising load demand necessitate optimized economic dispatch. The real world ED (Economic Dispatch) is highly non-convex, nonlinear and discontinuous...

De-Centralized Multi Robot Co-Ordination and Communication

The aim of this research is to develop a decentralized communication system of multiple robots which have capability to communicate and coordinate with each other, by which all robots work individually while keeping conn...

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

Download PDF file
  • EP ID EP191399
  • DOI -
  • Views 149
  • Downloads 0

How To Cite

Muhammad Abdil Basit Ur Rahim, Fahim Arif (2016). Translating Activity Diagram from Duration Calculus for Modeling of Real-Time Systems and its Formal Verification using UPPAAL and DiVinE. Mehran University Research Journal of Engineering and Technology, 35(1), 139-154. https://europub.co.uk/articles/-A-191399