Abstract:
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.
Keywords:real-time systems, models of multitask software systems, task interfaces, dynamic correctness of software applications.