On the verification of open distributed systems
Mads Dam, Lars‐Åke Fredlund · 1998
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 procees networks with a changing intercounection 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 program, in this fragment The specification logic extends the firstorder /J-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 hilling agent which controls and charges for user access to a given resource. IntroductionA central feature of open distributed systems as opposed to concurrent systems in general is their reliance on modularity.Open distributed systems must accommodate addition of new components, modification of interconnection structure, and replacement of existing components without affecting overall system behaviour adversely.To this effect it is important that component interfaces are clearly defined, and that systems can be put together relying only on component behaviour along these interfaces.That is, behaviour specification, "Work partially supported by the Computer Science Laboratory of EHc~on Telecom AB, Stockholm, EU EIprit BIIA project 8130 LOMAPS, and • Swedish Found•tion for Str•tegic Re~.