Premium
Development of an atomic‐broadcast protocol using LOTOS
Author(s) -
James Perry R.,
Endler Markus,
Gaudel MarieClaude
Publication year - 1999
Publication title -
software: practice and experience
Language(s) - English
Resource type - Journals
SCImago Journal Rank - 0.437
H-Index - 70
eISSN - 1097-024X
pISSN - 0038-0644
DOI - 10.1002/(sici)1097-024x(19990710)29:8<699::aid-spe255>3.0.co;2-f
Subject(s) - computer science , formal specification , formal methods , language of temporal ordering specification , protocol (science) , programming language , specification language , commit , service (business) , semantics (computer science) , software engineering , communications protocol , programming language specification , formal description , operating system , database , programming paradigm , pathology , medicine , alternative medicine , inductive programming , economy , programming domain , economics
In this article we report on the development of a group‐communication service using the formal specification language LOTOS, and present our experience in using publicly available tools for this purpose. The service implements atomic broadcast through a Two‐Phase‐Commit protocol, providing at‐least‐once delivery semantics and with no restriction on message delivery order. First we wrote an informal specification describing the desired properties from the service, the interfaces with the underlying network layer and the upper user layer, and the protocol to be used by the service. Then we developed the formal specification of the protocol in LOTOS. After validating the formal specification and thus having a certain confidence in its adequacy with respect to the informal specification, we derived test cases from the formal specification and implemented the service using the Concert/C distributed programming language. While testing the implementation, we found that most errors were related to unspecified features or bugs in the execution environment. From this experience, we draw our conclusions on the usefulness of software development based on formal techniques. Copyright © 1999 John Wiley & Sons, Ltd.