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 99
- Downloads 0
An Improved Data Model for Uncertain Data
Uncertain data can be categorized as imprecise data and probabilistic data. In each of these categories, the uncertainty can be found at different granularity levels. Conventional data models are developed for the purpos...
Implementation of Cavity Perturbation Method for Determining Relative Permittivity of Non Magnetic Materials
Techniques for the cavity measurement of the electrical characteristics of the materials are well established using the approximate method due to its simplicity in material insertion and fabrication. However, the exact m...
Analysis of Formal Methods for Specification of E-Commerce Applications
E-commerce based application characteristics portray elevated dynamics while incorporating decentralized nature. Extreme emphasis influencing structural design plus implementation, positions such applications highly appr...
Effect on Compressive Strength of Concrete Using Treated Waste Water for Mixing and Curing of Concrete
Effective utilization of the available resources is imperative approach to achieve the apex of productivity. The modern world is focusing on the conditioning, sustainability and recycling of the assets by imparting innov...
Effect of Intercritical Heat Treatment on Mechanical Properties of Reinforcing Steel Bars
Intercritical heat treatments attempts were made to enhance the mechanical properties of reinforcing steel bars milled from scrap metal. For this, two grades of steel bars were obtained from different steel mills and the...