@book {IOPORT.05195115, author = {Szpyrka, Marcin}, title = {Design and analysis of embedded systems with RTCP-nets. (Modelowanie i analiza system\'ow wbudowanych z zastosowaniem RTCP-sieci.)}, year = {2007}, pages = {157~p.}, publisher = {Krak\'ow: AGH Uczelniane Wydawnictwa Naukowo-Dydaktyczne}, abstract = {Summary: The main purpose of this dissertation is to present an extended description of RTCP-nets. It contains both theoretical bases of this formalism and also information about possibilities of practical applications. RTCP-nets are the main and original result of adaptation of timed coloured Petri nets for modelling of real-time systems. They are a subclass of coloured Petri nets, but they use a different time model, transitions priorities, and modified rules of the design of hierarchical models. One of the main advantages of RTCP-nets is the possibility of modelling of embedded systems, the functionality of which is based on rule-based systems. The theoretical part of this dissertation contains formal definition of the RTCP-nets and description of analysis methods. Especially, it focuses on dynamic aspects of such systems connected with the new time model introduced in the dissertation. The most important results are given in chapter 4. The chapter deals with coverability graphs that are basis of the main formal analysis method for RTCP-nets. It has been shown in the chapter that for a strongly bounded RTCP-net there exists a finite coverability graph, which is very important from a practical point of view. Practical aspects of the presented approach are elaborated in the second part of the dissertation. It contains description of a method of the design of hierarchical models and an algorithm for a semi-automatic transformation from a model into an implementation in Ada 2005 programming language. The key idea introduced in this part is the canonical form of hierarchical nets. An RTCP-net in the canonical form represents the structure of a modelled system, its dynamic and also functional relationships. Each part of the modelled system and each system activity is represented by a distinguished part of the corresponding net. Hence, it is possible to generate some parts of the model automatically and also to identify fragments of Ada source code that should be defined e.g.: tasks, protected objects, suspending objects, etc. This part of the dissertation contains also an example of application of the RTCP-nets for modelling of embedded systems. A railway traffic management system for a real train station was used for this purpose.}, identifier = {05195115}, }