------------------------------------------------------------------------------- \_\_\_ \_ \_ \_\_\_\_\_ \_ \_ Rheinisch- Aachen \_ \_ \_ \_ \_ \_ \_ Westfaelische University \_\_\_ \_ \_ \_ \_ \_\_\_\_ Technische of Technology \_ \_ \_\_ \_\_ \_ \_ \_ Hochschule \_ \_ \_ \_ \_ \_ \_ Aachen _______________________________________________________________________________ Dept. of Computer Science Announcements of new Technical Reports 8/00 ------------------------------------------------------------------------------- WWW at URL: ftp://ftp.informatik.rwth-aachen.de/pub/reports/index.html ~~~~~~~~~~~ Anonymous ftp: ftp.informatik.rwth-aachen.de(137.226.225.3):/pub/reports ~~~~~~~~~~~~~~ Format: gzipped PostScript Files (<number>.ps.gz) ______________________________________________________________________________ TITLE = Verifying Generic Erlang Client-Server Implementations NUMBER = 00-08 AUTHORS = Thomas Arts and Thomas Noll PAGES = 26 ABSTRACT = The Erlang Verification Tool is an interactive theorem prover tailored to verify properties of distributed systems implemented in 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 demonstrate our approach by developing a verification method for client-server systems designed using the generic server implementation of the Open Telecom Platform. Our idea is to specify a set of transition rules which characterize the abstract behaviour of the generic server functions. In this way we can reason in a compositional way about any client-server application without having to consider the concrete implementation details of the generic part, which simplifies proofs dramatically. We argue that, due to the generality of our approach, it is easily possible to put it into practice using other verification tools or to integrate further generic architectural elements such as finite-state machines or event handlers. KEYWORDS = software verification, theorem proving, formal semantics This report is located at ftp://ftp.informatik.rwth-aachen.de/pub/reports/2000/00-08.ps.gz _______________________________________________________________________________ If you are interested in receiving periodic announcements, subscribe to our mailing-list. Write an e-mail with subject subscribe (your e-mail address) to tr-announce-request@informatik.rwth-aachen.de TR-Admin tr-admin@informatik.rwth-aachen.de