Specifying Software/Hardware Interactions in Distributed Systems

This paper describes a system level specification approach that enables the designer to formulate and answer questions regarding the system\u27s logical correctness and performance characteristics when the interaction between the hardware and the software is important, i.e., when the impact of faults, failures, communication delay, hardware selection, scheduling policies, etc., must be considered. In the simplest terms, our concern extends beyond the traditional software correctness questions by addressing the issue of employing logical verification techniques to determine software correctness and performance characteristics when running on a particular distributed hardware architectures and using a particular operating system. A language called CSPS (an extension of Hoare\u27s CSP) is used in the illustration of the approach. Employing CSP as a base allows modelled systems to be verified using techniques already developed for verifying CSP programs