Itinarary nets – the graphical formalism for presentation of real-time sofware application strucrures

A graphic formalism «itinerary nets» is expounded for representation of real–time software application structures. The formalism is oriented to verification of static and dynamic properties of task interfaces. The bounds are defined for applicability of verification that is based on using of states and transitions graphs. A method is defined for assessing the value of blocking factor in systems with concatenated critical intervals of access to shared resources. The method is based on introduce of task profile feature.