Colored Petri Net-based Modeling and Formal Analysis of Component-based Applications.
Pranav Srinivas Kumar, Abhishek Kumar Dubey, Gábor Karsai · 2014
Abstract. Distributed Real-Time Embedded (DRE) Systems that ad-dress 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 re-quirements, 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, de-pendable and safe operation upon deployment. This paper describes how we can model and analyze applications for these systems in order to ver-ify 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 verification-driven workflow wherein the application model can be refined and restructured before actual code development. 1