Time aspects play an essential role in real-time systems. One of the most often used techniques of designing real-time systems is the timed statecharts (TSCs) technique. In this paper, new timed statecharts based on UML notation are introduced. The main difference between the UML statecharts and the TSCs presented in the paper is the pair of minimal and maximal execution times assigned to states of the TSCs. Additionally, any interaction can be characterized by its minimal and maximal duration time. Moreover, the paper presents semantics for TSCs, emphasizing time aspects rather than variable valuation. The minimal and maximal execution time problem (MMETP) for TSCs is defined and the computational complexity of the MMETP is studied. It is proven in this paper that there is a limit between such TSCs for which there exists a polynomial algorithm for MMETP and such TSCs for which MMETP remains NP-hard. The mentioned limit is located between the AND state with any number of XOR states that are expressed by simple paths without guards and the AND state with two XOR states with no limitations. Since the MMETP is NP-hard, it is reasonable to use structural reductions of TSCs. A Theorem that is the theoretical foundation of a program loop reduction is proven.

The paper contains extensions of specification language LOTOS in three directions: time-consuming actions, real-time and performance evaluation constructions. Time-consuming actions seem to be more natural than instantaneous actions and they are well suited for real-time system specification and for its performance evaluation. The notions of beginning and termination of the time-consuming action enable to impose time restrictions on beginning and termination times of activities. From performance evaluation point of view it is often important to know explicit how long a specific action has been executed (not when the action has been completed only). We have also introduced a time-out as a specific action. An expressive power of this action has been discussed. We have defined such a performance evaluation extension of LOTOS that can be used as a modelling language for performance evaluation of distributed systems. A true concurrency semantics (in the sense that it refers to the fact that actions with durations may overlap in time) for this extension is defined.

In the field of distributed computer systems, in order to specify, verify, and implement systems formally, Formal Description Techniques have been developed. Specification language Estelle, which is an ISO standard, is one of these techniques. Purpose of the present paper is to create a method of performance evaluation for the language Estelle that is based on Petri net methodology. The paper is oriented towards partially automatic generation of performance model for a distributed system - having Estelle specification of this system. A method for finding the performance characteristics of system defined in Estelle is given too.

Timed Petri nets are useful in performance evaluation of concurrent systems. The maximum computation rate is achieved for minimal cycle time of timed Petri net. It is known that minimal cycle time problem for P-invariant Petri nets is NP-complete. In this paper we prove that the minimal cycle time problem, for non-P-invariant Petri nets and for a small subclass of P-invariant Petri nets called free-choice nets having live and safe marking, is NP-complete.