A LOTOS extension for the performance analysis of distributed systems

1 April 1994

journal article
Published by Institute of Electrical and Electronics Engineers (IEEE) in IEEE/ACM Transactions on Networking

Vol. 2 (2) , 151-165
https://doi.org/10.1109/90.298433

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 i

Keywords

This publication has 13 references indexed in Scilit:

Introduction to the ISO specification language LOTOS
Published by Elsevier ,2003
Reactive, generative, and stratified models of probabilistic processes
Published by Institute of Electrical and Electronics Engineers (IEEE) ,2002
LOTOS-like process algebras with urgent or timed interactions
Published by Elsevier ,1992
Bisimulation through probabilistic testing
Information and Computation, 1991
A calculus for communicating systems with time and probabilities
Published by Institute of Electrical and Electronics Engineers (IEEE) ,1990
The effect of execution policies on the semantics and analysis of stochastic Petri nets
IEEE Transactions on Software Engineering, 1989
An integrated algorithm for probabilistic protocol verification and evaluation
Published by Institute of Electrical and Electronics Engineers (IEEE) ,1989
A timed failures model for extended communicating processes
Published by Springer Nature ,1987
A Performance Model of the OSI Communication Architecture
IEEE Transactions on Communications, 1986
Performance Analysis Using Stochastic Petri Nets
IEEE Transactions on Computers, 1982