Formal specification and analysis of distributed systems

The paper deals with the problems that arise while developing software of such distributed systems as real-time, computer network protocols and distributed information-processing systems. In the introduction, some essential peculiarities typical of distributed systems (DS) and a general scheme for developing such systems are presented. The main idea of this paper is the use of a piece-linear aggregate mathematical method for formal specification, simulation and validation of DS. The main advantage of this approach is that it integrates two tasks of differing nature, i.e. simulation and correctness analysis of specification, on the basis of a single specification. The method of a transformation of aggregate specification to the first-order predicates and its further use for the correctness analysis of the aggregate specification using logic-based programming will also be presented. It will also be shown how to transform an informal description of system functioning to aggregate specification using production rules. The presented methods are explained using illustrative examples.