Real-time and performance evaluation extensions of specification language LOTOS

The paper contains extensions of specification language LOTOS in three directions: actions with durations, real-time and performance evaluation constructions. We have 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 these extensions is defined