In: IEEE-ACM Trans. on Networking, Vol. 2, No. 2, pages 151-165. 1994.
Abstract: Performance analysis and formal correctness verification of computer communication protocols and distributed systems have traditionally been considered as two separate fields. However, their integration can be achieved by using formal description techniques as paradigms for the development of performance models. This paper presents a novel extension of LOTOS, one of the two formal specification languages that were standardized by ISO. The extension is specifically conceived to integrate performance analysis and formal verification. The extended language syntax and semantics are formally defined, along with a mapping from extended specifications to performance models. The mapping preserves the specified observable behavior. Two simple examples, a stop-and-wait protocol and a time-sharing system, are used to concretely demonstrate the new approach and to validate it.
Keywords: LOTOS, correctness verification, formal correctness, performance analysis, stochastic Petri nets.