Pranav Srinivas Kumar, Abhishek Dubey, Gabor Karsai
Proceedings of the 11th Workshop on Model-Driven Engineering, Verification and Validation co-located with 17th International Conference on Model Driven Engineering Languages and Systems, MoDeVVa@MODELS 2014, Valencia, Spain, September 30, 2014 2014
Verifying properties of complex distributed applications requires formal methods that capture both scheduling and behavioral aspects. This work is innovative because it provides unified formal framework using Colored Petri Nets that integrates component scheduling with application semantics. The approach enables early detection of timing and functional violations.
This paper presents Colored Petri Net-based modeling and formal analysis approach for component-based applications in distributed real-time embedded systems. The methodology enables verification of system properties including deadline violations and buffer overflows through formal analysis. The approach integrates component operation scheduling with business logic modeling.
The Colored Petri Net approach successfully models component-based applications and verifies system properties through formal analysis. Testing demonstrates the methodology's ability to identify scheduling violations and potential deadlock conditions. Results support use of formal methods in verifying safety-critical distributed systems.
@inproceedings{Kumar2014,
author = {Kumar, Pranav Srinivas and Dubey, Abhishek and Karsai, Gabor},
booktitle = {Proceedings of the 11th Workshop on Model-Driven Engineering, Verification and Validation co-located with 17th International Conference on Model Driven Engineering Languages and Systems, MoDeVVa@MODELS 2014, Valencia, Spain, September 30, 2014},
title = {Colored Petri Net-based Modeling and Formal Analysis of Component-based Applications},
year = {2014},
pages = {79--88},
abstract = {Distributed Real-Time Embedded (DRE) Systems that address safety and mission-critical system requirements are applied in a variety of domains today. Complex, integrated systems like managed satellite clusters expose heterogeneous concerns such as strict timing requirements, complexity in system integration, deployment, and repair; and resilience to faults. Integrating appropriate modeling and analysis techniques into the design of such systems helps ensure predictable, dependable and safe operation upon deployment. This paper describes how we can model and analyze applications for these systems in order to verify system properties such as lack of deadline violations. Our approach is based on (1) formalizing the component operation scheduling using Colored Petri nets (CPN), (2) modeling the abstract temporal behavior of application components, and (3) integrating the business logic and the component operation scheduling models into a concrete CPN, which is then analyzed. This model-driven approach enables a verication-driven workow wherein the application model can be rened and restructured before actual code development.},
bibsource = {dblp computer science bibliography, https://dblp.org},
biburl = {https://dblp.org/rec/bib/conf/models/KumarDK14},
category = {workshop},
contribution = {colab},
keywords = {Colored Petri Nets, formal analysis, component-based systems, scheduling verification, real-time systems},
project = {cps-reliability,cps-middleware},
tag = {platform},
timestamp = {Tue, 28 May 2019 16:23:34 +0200},
url = {http://ceur-ws.org/Vol-1235/paper-10.pdf}
}