LVT: a layered verification technique for distributed computing systems

摘要

This paper presents a layered verification technique, called LVT, for the verification of distributed computing systems with multiple component layers. Each lower layer in such a system provides services in support of functionality of the higher layer. By taking a very general view of programming languages as interfaces of systems, LVT treats each layer in a distributed computing system as a distributed programming language. Each relatively higher-level language in the computing system is implemented in terms of a lower-level language. The verification of each layer in a distributed computing system can then be viewed as the verification of implementation correctness for a distributed language. This paper also presents the application of LVT to the verification of a distributed computing system, which has three layers: a small high-level distributed programming language; a multiple processor architecture consisting of an instruction set and system calls for inter-process message passing; and a network interface. Programs in the high-level language are implemented by a compiler mapping from the language layer to the multiprocessor layer. System calls are implemented by network services. LVT and its application demonstrate that the correct execution of a distributed program, most notably its inter-process communication, is verifiable through layers. The verified layers guarantee the correctness of (1) the compiled code that makes reference to operating system calls, (2) the operating system calls in terms of network calls, and (3) the network calls in terms of network transmission steps. The specification and verification involved are carried out by using the Cambridge Higher Order Logic (HOL) theorem proving system. Copyright © 1999 John Wiley & Sons, Ltd.