Title
Verifying Generic Erlang Client-Server Implementations
Abstract
The Erlang Verification Tool is an interactive theorem prover tailoredto verify properties of distributedsystems implementedin Erlang. It is being developed by the Swedish Institute of Computer Science in collaboration with Ericsson. In this paper we present an extension of this tool which allows to reason about the Erlang code on an architectural level. We present a verification methodfor client-server systems designedusing the generic server implementation of the Open Telecom Platform. For this purpose, we specify a set of transition rules which characterize the abstract behaviour of the generic server functions. By this means we can reason in a partitionedw ay about any client-server application without having to consider the concrete implementation details of the generic part, which simplifies proofs dramatically. The generic server architecture is just an example, andthe technique extends to many other generic components. Moreover, the idea of considering standard components to reason on the architectural level of a concrete implementation can also be exploredwhen using other verifications tools for Erlang or in the context of another language.
Year
DOI
Venue
2000
10.1007/3-540-45361-X_3
IFL
Keywords
Field
DocType
generic server implementation,generic part,generic component,erlang code,generic server function,concrete implementation detail,architectural level,erlang verification tool,verifying generic erlang client-server,concrete implementation,generic server architecture,client server,finite state machine,system design,distributed system,theorem prover
Architecture,Programming language,Computer science,Erlang (programming language),Theoretical computer science,Implementation,Mathematical proof,Selection rule,Client–server model,Proof assistant
Conference
Volume
ISSN
ISBN
2011
0302-9743
3-540-41919-5
Citations 
PageRank 
References 
7
0.78
5
Authors
2
Name
Order
Citations
PageRank
Thomas Arts116515.66
Thomas Noll2236.12