Engineering an Implementation of the OSI CCR Protocol Using the Information211 Systems Techniques of Formal Specification and Program Transformation

摘要

The overall objective of the project was to engineer a C implementation of an211u001eOpen Systems Interconnection (OSI) protocol on a Unix platform. This document 211u001edescribes the authors' experience of engineering the implementation of the CCR 211u001e(Comitment, Concurrency and Recovery) protocol using formal methods. The target 211u001elanguage was C, and the formal sepcification language used was LOTOS. The method 211u001eused was te Lotosphere method and the outputs from the process were: a C 211u001eimplementation of the CCR protocol, and a set of generalized transformation rules 211u001efor generating C code from LOTOS specifications. The aim of the project was to 211u001eapply sound information systems engineering priniciples to the problem using the 211u001etechniques of formal specification, prototyping and program transformation to 211u001eensure that the implementation met professional standards of quality in terms of 211u001ecorrectness, efficiency, portability and maintainability.