On the Verification of Open Distributed Systems

Dam, Mads and Fredlund, Lars-Åke (1997) On the Verification of Open Distributed Systems. [SICS Report]



A logic and proof system is introduced for specifying and proving properties of open distributed systems. Key problems that are addressed include the verification of process networks with a changing interconnection structure, and where new processes can be continuously spawned. To demonstrate the results in a realistic setting we consider a core fragment of the Erlang programming language. Roughly this amounts to a first-order actor language with data types, buffered asynchronous communication, and dynamic process spawning. Our aim is to verify quite general properties of programs in this fragment. The specification logic extends the first-order $\mu$-calculus with Erlang-specific primitives. For verification we use an approach which combines local model checking with facilities for compositional verification. We give a specification and verification example based on a billing agent which controls and charges for user access to a given resource.

Item Type:SICS Report
Uncontrolled Keywords:Open Distributed Systems, Program Verification, Erlang, Parametric Verification, Agents
ID Code:2161
Deposited By:Vicki Carleson
Deposited On:22 Oct 2007
Last Modified:18 Nov 2009 16:00

Repository Staff Only: item control page