Networks and Distributed Systems
Research group of Prof. Peter Bernard Ladkin, Ph.D.
Formal Software Development for Control of a Biological Cell-Fermentation Reactor
Lutz Sommerfeld and Peter B. Ladkin
This project concerns the specification of and control-software development for of a 20-liter fermentation-reactor used to grow large-scale cell cultures in the Biotechnology section of the Faculty of Technology. The reactor is already partly digitally controlled, and further aspects of the control are to be digitised.The Specification in TLA+
The first part of the project to be completed is the specification of the device and its control It is necessary for reasonable software development and maintenance that the device and its control be formally described. We describe the device and its high-level control in the logical specification language TLA+.This system is an example of a so-called `hybrid system' in that it is partly digital, partly `physical'. The specification problem distinguishes itself from other hybrid-system specification problems in that the biological process which governs the operation of the reactor is vague, and the reaction is not guaranteed always to succeed. Thus there are no precise differential equations or other mathematical specifications that describe the system that we are able to use in the specification. The specification must nevertheless provide a rigorous basis for control software development.
The specification, its structure and its justification may be found in the Diplom Thesis (in German, 75pp) [ DVI 80K gzipped | PS 219K gzipped ] of Lutz Sommerfeld, submitted 11 July 1997. Individual modules of the TLA+ specification are as follows:
General definitions:
Specific modules for the reactor and its process:
Specific modules for software control:
A précis of this work was presented at the German National Conference 7. GI/ITG-Fachgespräch, Formale Beschreibungstechniken für verteilte Systeme, in Berlin, 19-20 June 1997, and are included in the Tagungsband (Proceedings). It appears in RVS Publications as Research Report RVS-RR-97-07 (in German) [ DVI 31K gzipped | PS 66K gzipped ]Further information about TLA und TLA+ may be found (in English) in Leslie Lamport's TLA Home Page, in RVS TLA publication abstracts, and in the lecture notes RVS-LN-06 (in German), Michael Blume's Introduction to TLA+ [ DVI | PS ]