Loading...

Extending Rebeca Modeling Language for Modeling and Analysis of UML/MARTE Diagrams

Mohajerani, Kiarash | 2025

282 Viewed
  1. Type of Document: M.Sc. Thesis
  2. Language: Farsi
  3. Document No: 58588 (19)
  4. University: Sharif University of Technology
  5. Department: Computer Engineering
  6. Advisor(s): Movaghar, Ali; Izadi, Mohammad
  7. Abstract:
  8. The design and analysis of real-time and embedded systems face complex challenges due to strict timing requirements. The UML/MARTE profile, as an industry standard, provides a rich, semi-formal language for modeling these systems. However, guaranteeing the correctness of critical properties necessitates precise formal analysis and verification of these models. Attempts to directly translate MARTE models into standard formal languages, such as Timed Rebeca, fail due to a deep "semantic gap." This gap stems from the absence of equivalent linguistic constructs in the target languages for MARTE's high-level analytical concepts, such as end-to-end scenarios, workload patterns, and scheduling policies, leading to the loss of the original model's "analytical intent." To bridge this gap, this research presents a comprehensive framework comprising two main innovations. First, "Extended Timed Rebeca" is introduced as a new formal modeling language that natively supports MARTE concepts by adding three key, first-class constructs: (1) "event sequences" for the explicit modeling of analytical scenarios and workload patterns; (2) "mailboxes" for the operational implementation of configurable scheduling policies; and (3) "parametric time ranges" for managing timing uncertainty. Second, a novel analysis methodology based on "Parametric Model Checking" (PMC) is developed, which leverages "symbolic-time" analysis and SMT solvers to overcome the state space explosion challenge arising from timing uncertainty. The efficacy and correctness of this framework are evaluated through comprehensive case studies. The results demonstrate that the schedulability verdict aligns with traditional static analysis methods, thereby validating the correctness of the transformation process. More importantly, the proposed method proves its superiority by providing rich "diagnostic feedback" through the generation of precise "counterexamples" in case of failure, thus closing the "diagnostic gap" inherent in static methods
  9. Keywords:
  10. Real Time System ; Formal Methods ; Unified Modeling Language (UML) ; Rebeca Modeling language ; Modeling and Analysis of Real-Time and Embedded Systems (MARTE) Profile ; Parametric Model Checking

 Digital Object List

 Bookmark

...see more