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:
Specific modules for the reactor and its process:
Specific modules for software control: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 ]