Specification and analysis of timing requirements in CBD approach using modular petri nets

Abstract

In real-time software, not only computation errors but also timing errors can cause system failures, which eventually result in significant physical damages or threats to human life. To efficiently guarantee the timely execution of expected functions, it is necessary to clearly specify and formally verify timing requirements before performing detailed system design. In this paper, we propose a systematic procedure for transforming and integrating timing scenarios into a Petri net-based model: Modular TER nets. And we provide a static analysis technique for checking inconsistencies and conflicts among timing constraints. Although our approach is based on the Modular TER nets, users only focus on describing timing requirements in the scenario concepts, since the detailed transformation and integration procedures based on Petri nets are hidden to users. By analyzing the generated formal model, users can easily check the timing inconsistencies among requirements before designing and implementing a system. On the other hand, with the expected benefit of reusability and extensibility, component technology has been gradually applied to developing industrial applications including real-time systems. However, most of component-based approaches applied to real-time systems lack in a systematic and rigorous approach to specifying and verifying timing requirements at an earlier development stage. This thesis also proposes a component-based approach to specifying and verifying timing requirements for real-time systems in a systematic and compositional manner. We first describe behaviors of the constituent components including timing requirements in UML diagrams, and then translate the UML diagrams into Modular TER nets, an extension of TER nets, to perform timing analysis in a compositional way. The merit of the proposed approach is that the specification and analysis results can be reused and independently maintained.