Beschreibung eines vagen Echtzeit-Hybrid-Systems in TLA^{+}

Lutz Sommerfeld  Peter Ladkin

AG Rechnernetze und Verteilte Systeme Technische Fakultät der Universität Bielefeld Universitätsstraße 25 33615 Bielefeld

Zusammenfassung

Diese Spezifikation beschreibt ein technischen Gerät, für das keine physikalisch oder mathmatisch genaue Beschreibung vorliegt. Es liegt lediglich eine vage, zum Teil umgangssprachliche Beschreibung der Zusammenhänge vor, da die genauen Prozeßparameter für die Durchführung der Kultivierung unbekannt sind und deren Bestimmung unnötig ist. Darin unterscheidet sich die Aufgabenstellung vom ”Steam Boiler Control Problem“. Die vorgestellte Lösung erfolgt auf einer möglichst hohen Abstraktionsebene, so daß die Prozeß-Umwelt-Modellierung als auch die Theorien zur logischen Form von artifacts berücksichtigt werden konnten. Als Spezifikationssprache wurde TLA^{+} gewählt.

1 Problembeschreibung

Der Ausgangspunkt dieser Spezifikation ist die Beschreibung eines Perfusions-Bioreaktors mit einem Fasssungsvermögen von 20 Litern in einer formalen Spezifikationssprache aus der Sicht des benutztenden Biologen. Ein solcher Bioreaktor wird vorzugsweise benutzt, um tierische Körperzellen zu kultivieren. Diese Zellen benötigen für einen schnelles und stetiges Wachstum eine dem natürlichen Lebensraum entsprechende Umgebung. Selbstverständlich hat ein solches Gerät eine ihm zugrunde liegende theoretische Basis (siehe z.B. [Pirt75]), auf der es entwickelt worden ist. Da sich jedoch dieser komplexe biologische Ablauf nur schwer in physikalischen bzw. mathematischen Modell beschreiben läßt, erfolgt die Feineinstellung der einzelnen Komponenten nach den erzielten Kultivierungserfolgen. Der gesamte Aufbau unterliegt daher einem stetigen, wenn auch nur geringen Wandel. So ist z.B. die regelungstechnische Bedeutung der eingestellten PID-Kennwerte für den Zelltechnologen nebensächlich. Er richtet alle Einstellungen danach aus, eine möglichst optimale Vermehrung zu erreichen, ohne sich mit der regelungstechnischen Analyse der Anlage auseinander zu setzen. Der Ansatz dieser Spezifikation ist daher nicht die exakte Beschreibung der technischen Anordnung und deren Einstellungen, sondern die umgangssprachliche Beschreibung der für den Zellwachstum wichtigen Bedingungen und deren Realisation mit den vorhandenen technischen Mitteln, aus der Sicht des die Anlage benutzenden Biologen. Diese Informationen wurden in mehreren Experteninterviews ermittelt. Es ist auf diese Weise möglich bei Veränderungen am Aufbau oder der Steuerung des Bioreaktoers festzustellen, ob die von den Biologen gewünschten Kriterien erfüllt werden. Das veränderte System wird nicht auf die Erfüllung eines technischen Modells überprüft, sondern auf die Erfordernisse, die vom Biologen als wichtig erachtet werden. Es wird demnach die rein physikalische Ebene des Geräts verlassen, und auf der abstrakteren Ebene der artifacts [Lad96] argumentiert. In diesem Punkt unterscheidet sich diese Spezifikation von den bisherigen Beschreibungen hybrider Systeme, wie z.B. das ”Steam boiler control specification problem“[ABL96], welches von Frank Leßke und Stephan Merz in TLA^{+} realisiert wurde. Dort liegt der Spezifikation ein mathematisch-eindeutig beschriebene Problemstellung zugrunde, welche hier nicht vorhanden ist.

2 Einführung

2.1 Was ist ein Artifact?

In [Sea96] wird beschrieben, daß es zur Beschreibung von artifacts nicht ausreichend ist, nur ihre physikalischen Eigenschaften zu berücksichtigen. Ein artifact ist demnach ein Gegenstand, welcher neben seiner physikalischen Existenz einen situationsabhängigen Zweck hat. So reicht z.B. die Beschreibung einer mit Tinte gefüllten Mine in einer Plastikhülle, an deren Spitze eine Kugel für die gleichmässige Verteilung der Tinte bei der Bewegung dieser Spitze über einer Oberfläche sorgt, nicht aus, um einen Kugelschreiber zu beschreiben. Erst durch den Zweck des Schreibens, welcher dem Kugelschreiber anhaftet, ist dieser vollständig beschrieben. Zwar gibt es auch Dinge, die nicht zur Klasse der artifacts gehören, deren Existenz nicht mit einem eindeutigen Zweck verbunden ist, z.B. der Mensch. Bei dem beschriebenen Bioreaktor handelt es sich jedoch unstrittig um ein artifact. Daher sollte in der formalen Beschreibung auch die Beschreibung des Zwecks enthalten sein.

2.2 Einführung in TLA+

Die hier benutzte Spezifikationssprache ist TLA^{+} [Lam95] . Es handelt sich um eine von Lamport entwickelte Sprache, die auf der Temporal Logic of Actions TLA[Lam94] basiert. Die Semantik von TLA^{+} kann mit dem Modell einer unendlichen Folge diskreter, zeitlich linearer Zustände beschrieben werden. Jeder Zustand definiert und unterscheidet sich über die den Zustandsvariablen zugewiesenen Werte. TLA^{+} Formeln lassen sich in vier verschiedene Klassen einteilen.

Temporale-Formeln enthalten temporale Operatoren, um über eine unendliche Folge von Zuständen Aussagen zu treffen. Die beiden wichtigsten temporalen Operatoren sind □ und ∃ ∃ ∃ ∃ ∃ ∃. □A besagt daß eine Aussage A für alle folgenden Zustände wahr ist. ∃ ∃ ∃ ∃ ∃ ∃ ist der temporale Existenzquantor (nicht zu verwechseln mit dem logischen ∃), welcher es erlaubt Zustandsvariablen innerhalb der Module zu erzeugen (hiding of internal variables). Ein weiterer wichtiger Operatoren ist ◇A =^{Δ} ¬□¬A. Er besagt, daß die Aussage A zumindest manchmal in der Zukunft erfüllt sein wird.

Action-Formeln beschreiben den Übergang von einem Zustand in den nächsten.^{1} Dem Namen der Variablen, welche den Wert im nächsten Zustand repräsentiert, wird ein prime angehängt. Durch x′ = x + 1 wird beschrieben, daß der Wert von x im folgenden Zustand um 1 erhöht ist. Folgende Bezeichnungen sind zu beachten:

• [A]_{e} bedeutet, daß entweder A eintritt, oder e ändert seinen Wert nicht.

• ⟨A⟩_{e} sagt aus, daß ein A Schritt stattfindet und e dabei verändert wird.

• Enabled A heißt, ein A Schritt ist möglich.

• unchanged e bedeuted, e verändert sich nicht.

Zustands-Formeln sind Formeln welche über einen bestimmten Zustand eine Aussage treffen. Sie enthalten keine geprimten Zustandsvariablen, z.B. y = x + 3.

Konstante-Formeln enthalten nur Konstanten, also keine Zustandsvariablen.^{2}

Desweiteren weist TLA^{+} einige syntaktische Eigenarten auf, die hier kurz erläutert werden.

1Als ”nächster Zustand“ wird in TLA^{+} der nächste Zustand bezeichnet, welcher sich von dem vorhergehenden durch den Inhalt mindestens einer Zustandsvariablen unterscheidet; d.h. TLA^{+} ist ”stuttering invariant“.

2Zwar können Konstanten einen beliebigen Wert annehmen, jedoch muß dieser in allen Zuständen unverändert bleiben. Hierin unterscheiden sich Konstanten von Zustandsvariablen.

Das Modul-Konzept. TLA^{+} Spezifikationen lassen sich in Module unterteilen, welche sich mit den Befehlen include und import einbinden lassen. Während import einer textuellen Ersetzung gleichkommt, lassen sich mit include mehrere Instanzen des selben Moduls unter verschiedenen Namen in einem Modul einbinden. So kann über eine Namenserweiterung (includeName.actionName) auf die in dem ”includeten“ Modul enthaltenen actions zugegriffen werden. Durch zusätzliche Neubenennung der Zustandsvariablen kann zwischen den Zustandsvariablen der verschiedenen Instanzen eindeutig unterschieden werden.

Tupel sind Funktionen. ^{3} Daher wird beides in TLA^{+} analog verwendet. So kann g[i] sowohl den Wert der Funktion^{4} g = [x ∈ S ↦ e] mit Argument i, als auch das i-te Element eines Tupels g = ⟨g_{1} … g_{n} ⟩ bedeuten.

Weiterreichende Informationen über TLA^{+} finden sich in [Lam94] und [Lam95].

2.3 Der Bioreaktor

Der hier beschriebene membranbegaste 20 Liter Bioreaktor wird über eine analoge elektronische Regelungstechnik gesteuert. Es existiert zusätzlich eine Schnittstelle zu einem PC, welcher mit einer speziellen Regelungssoftware zur Begasungssteuerung ausgestattet ist, die es erlaubt zwischen einer klassischen PID-Regelung und einer benutzerdefinierbaren Fuzzy-Regelung zu wählen. Abgesehen von der Nährlösung, ist die Begasung des Kulturmediums von größter Bedeutung für das Zellwachstum. Zu diesem Zweck befindet sich im Kulturmedium eine Membran, durch die das Gasgemisch in das flüssige Medium gelangt. Dieses Gas setzt sich aus den vier Komponenten Luft, O_{2}, N_{2} und CO_{2} zusammen. Mittels CO_{2} wird der pH-Wert des Kulturmediums reguliert. Luft und O_{2} dienen dazu, die Luftsättigung (pO_{2}) im Medium auf einem bestimmten Sollwert zu halten. Da die Tierzellen Sauerstoff verbrauchen und in CO_{2} umwandeln, ist es mit steigender Anzahl an Zellen notwendig, den CO_{2} Anteil zu veringern und den Luft bzw. O_{2} Anteil des Gasgemischs zu erhöhen, um einen Konstanten pH bzw. pO_{2} Wert zu erreichen. Damit, trotz schwankender Anteile von Luft, O_{2} und CO_{2}, ein konstanter Gasdurchfluß gehalten werden kann, wird N_{2} als Füllstoff verwendet, denn es hat keinen Einfluß auf den Kultivierungsprozeß. Zusätzlich zur Membranbegasung gibt es noch die Möglichkeit den Kopfraum oberhalb des Kulturmediums mit Luft oder der Membrangasmischung zu begasen. Für die Kultivierung ist es weiterhin wichtig, mittels einer Heizung eine bestimmte Temperatur im Medium zu halten. Um eine homogene Verteilung aller Inhaltsstoffe zu gewährleisten, gibt es einen Rotor, welcher das Medium durchmengt. Nähere Einzelheiten zur Kultivierung tierischer Zellen mit diesem Bioreaktor finden sich in [Lüt93].

3 Die Spezifikation

Anhand der Module Kontrolle ( Abbildungen 1, 2, 3 auf S. 6, 7, 8) und Kultivierung (Abbildung 5 auf S. 9) soll exemplarisch die Vorgehensweise bei der Umsetzung des Expertenwissens in eine TLA^{+} Spezifikation erläutert werden. Zunächst werden jedoch kurz die anderen Module in ihrem Inhalt und ihrer Funktion beschrieben. Auf die Darstellung der eigentlichen TLA^{+} Spezifikation dieser Module, wurde aus Platzgründen verzichtet. Sie können jedoch unter [SL97] eingesehen werden.

3.1 Modul Echtzeit

Für den Kultivierungsprozeß gelten zeitliche Bedingungen, innerhalb derer Veränderungen an den Zustandsvariablen stattfinden. Auch wenn die kritischen Zeitabschnitte nicht im Bereich von Sekundenbruchteilen liegen, sondern vielmehr im Bereich von Minuten bis Stunden, so handelt es sich bei der Kultivierung denoch um einen Echtzeitprozeß. Das Modul Echtzeit beschreibt die Behandlung von Echtzeit und timer in TLA^{+} , wie sie von Abadi und Lamport in [Lam93] und [AL94] vorgeschlagen wird. Die meisten Zustandsvariablen sind Größen, die sich nur kontinuierlich ändern können. Andere wiederum, wie z.B. die Anzahl der Zellen, können sich nur diskret verändern. Das Modul beschreibt diese Bedingungen, so daß sie in den anderen Modulen verwendet werden können.

3Ein n-Tupel kann als endliche Funktion mit einer n elementigen Definitionsmege aufgefaßt werden, deren n Funktionswerte die Elemente des n-Tupels sind.

4Für Werte die nicht in der Definitionsmenge S liegen, liefert die Funktion g einen undefinierten Wert.

3.2 Modul Umgebung

Der Bioreaktor befindet sich in einer Umgebung, die Einfluß auf den Prozeß der Zellvermehrung haben kann. Damit die Zellkultivierung nicht beeinträchtigt wird, sollte die Lichteinwirkung und die Raumtemperatur innerhalb vorgegebener Grenzen bleiben.

3.3 Modul Medium

Ein Bestandteil des Kultivierungsvorganges ist das Kulturmedium. Da es unabhängig von den anderen Teilen betrachtet werden kann, ist es in einem eigenständigen Modul beschrieben. Die in dem Kulturmedium enthaltenen Stoffe sind:

• Tierzellen zur Vermehrung, sowie abgestorbene Zellen.

• Ein Basalmedium, welches ein Gemisch aus vielen für die Kultivierung wichtigen Zutaten ist. Es wird durch eine Funktion dargestellt, welche zu jeder Zutat deren Menge im Basalmedium angibt.

• Bakterien sollten zwar während der gesamten Kultivierung nicht in das Kulturmedium gelan-

gen, sind aber nicht vollständig auszuschliessen. Die mit dem Kulturmedium verbundenen physikalischen Größen sind:

• Der pH-Wert

• Der pO2-Wert (Luftsättigung im Kulturmedium)

• Die Temperatur des Kulturmediums Das Modul Umgebung wird eingebunden, da diese auf das Medium einwirkt. Nach der Initialisierung der Zustandsveriablen ist beschrieben, auf welche Art sich diese verändern können.

• Zellen können sich durch Wachstum vermehren

• Zellen können absterben

• Das Basalmedium wird durch die Zellen verbraucht

• Der pH-Wert kann sich verändern

• Der pO2-Wert kann sich verändern

• Das Kulturmedium kann sich abkühlen

3.4 Modul Bioreaktor

Der Bioreaktor weist die zur Einwirkung auf das in ihm enthaltene Kulturmedium nötigen Einrichtungen auf. Er kann, wie auch das Kutlurmedium, als eigenständiger Bestandteil des Gesamtsystems in einem eigenen Modul beschrieben werden. Die den Bioreaktor beschreibenden Zustandsvariablen sind:

• Die Rührerdrehzahl des mit der Begasungsmembran umwickelten Rührers

• Die Gasmischung (Luft,O_{2}, CO_{2}, N_{2}) in der Begasungsmembran und im Kopfraum über dem Kulturmedium • Der Gasdruck in der Begasungsmembran und im Kopfraum

• Die Flußgeschwindigkeit des Gases in der Begasungsmembran und im Kopfraum

• Das Volumen des Kulturmediums

In dem Bioreaktor befindet sich das Kulturmedium, daher wird das Modul Medium eingebunden. Der Initialisierung folgt die Beschreibung der Einwirkungsmöglichkeiten des Bioreaktors auf das Kulturmedium.

• In den Bioreaktor können unabhängig von einander sowohl neues Basalmedium, als auch neue Zellen eingebracht werden

• Eine Entnahme von Kulturmedium ist möglich

• Bei diesen Vorgängen ist eine Verseuchung mit Bakterien nicht auszuschließen

• Das Kulturmedium kann erwärmt werden

• Die Rührerdrehzahl kann verändert werden

• Die Mischung des Gases in der Membran kann verändert werden

• Es kann gewählt werden zwischen der Begasung des Kopfraumes mit Luft oder dem Gasgemisch, welches in der Membran ist

• Die Gasflußgeschwindigkeit in der Membran und im Kopfraum kann einzeln verändert werden

• Der Druck in der Membran und im Kopfraum kann einzeln verändert werden

Es ist beschrieben, daß von den oben aufgezählten Veränderungshandlungen nur das Nachfüllen, die Entnahme und die Verseuchung direkt am Bioreaktor stattfinden können. Alle anderen Veränderungen müssen über die Einstellungen an der Kontrolleinheit erfolgen und werden daher dort ausgeführt.

3.5 Modul Kontrolle

In Abbildung 1 auf der nächsten Seite, werden im Abschnitt parameters die an der Kontrolle beteiligten Zustandsvariablen und Konstanten definiert. Die mit dem hochgestellten Index s versehenen Variablen stehen für die eingestellten Sollwerte der Zustandsvariablen. Die mit Δ beginnenden Konstanten repräsentieren die maximale Zeitspanne, innerhalb derer vom Sollwert abgewichen werden darf, ohne daß ein negativer Einfluss auf das Wachstum der Zellkultur entsteht. Die übrigen Konstanten sind die Initialisierungswerte für die Sollwerte. Im Abschnitt definitions werden zur besseren Übersicht alle Sollwerte in einem Tuppel sollVars zusammengefasst. Nachfolgend werden die Module Echtzeit und Bioreaktor eingebunden. Dies ist sinnvoll, da sich die Steuerung auf den Bioreaktor bezieht und zur Einhaltung der oben genannten Zeiten, der im Echtzeit Modul definierte timer, Abbildung 4 auf Seite 9, benutzt wird. Unter predicates werden die Sollwerte mit den dazugehörigen Werten initialisiert. Abbildung 2 auf Seite 7 zeigt die actions, welche zur Änderung der zur Kontrolle gehörenden Zustandsvariablen dienen. Zunächst kann jeder Sollwert auf einen neuen Wert eingestellt werden. Die Wertebereiche sind je nach Sollwert eingeschränkt. Die beiden letzten actions tragen dem Umstand Rechnung, daß der pH und der pO_{2} Wert nicht direkt, sondern nur indirekt über die Einstellung der Gasmischung beeinflusst werden kann. Im einzelnen wird beschrieben, daß eine Abweichung vom Sollwert im momentanen Zustand existiert. Das Mambrangas wird mit den entsprechenden Werten eingestellt und die Kopfraumbegasung wird so gewählt, daß im nächsten Zustand der Sollwert erreicht wird. Dies entspricht der Aussage, ”Bei nicht eingehaltenem Sollwert, soll durch Einstellung der Gasmischung, der Sollwert wieder ereicht werden.“ Wichtig für die Kultivierung von lebenden Zellen ist es, daß das Kulturmedium von

module Kontrolle Teil 1

parameters pH , pO_{2}, temperatur, ruehrerdrehzahl : Real^{0^{+}} variable membrandruck, membrangasfluss : Real^{0^{+}}variable kopfraumdruck, kopfraumgasfluss : Real^{0^{+}}variable pH^{s}, pO_{2}^{s}, temp^{s}, drehz^{s}, mDruck^{s}, mFluss^{s}, kDruck^{s}, kFluss^{s} : variable Δ_{pH} , Δ_{pO_{2}} , Δ_{temp} , Δ_{drehz} , Δ_{mDruck} , Δ_{kDruck} , Δ_{mFluss} , Δ_{kFluss} : constant pH _{0}^{s}, pO_{2}_{(0)}^{s}, temp_{0}^{s}, drehz_{0}^{s}, mDruck_{0}^{s}, mFluss_{0}^{s}, kDruck_{0}^{s}, kFluss_{0}^{s} : constant

definitions sollVars =^{Δ} ⟨pH^{s}, pO_{2}^{s}, temp^{s}, drehz^{s}, mDruck^{s}, mFluss^{s}, kDruck^{s}, kFluss^{s} ⟩

import Echtzeit

include Bioreaktor as reaktor

predicates Init =^{Δ} ∧ pH^{s} = pH _{0}^{s} ⋮ ∧ kFluss^{s} = kFluss_{0}^{s}

Tabelle 1: Modul Kontrolle, 1. Teil

den vorgegebenen Sollwerte nicht länger als einen maximalen Zeitraum abweicht. In Abbildung 3 auf Seite 8 wird nun auf diesen temporalen Aspekt der Steuerung eingegangen. Zunächst wird für alle zeitkritischen Zustandsvariablen mit Hilfe eines timers (VTimer) beschrieben, daß in allen Zuständen der neu geschaffene timer x = ∞ ist, wenn die Zustandsvariable dem Sollwert entspricht. Ansonsten ist x gleich dem ”Jetztzeitpunkt“ (now) plus der maximalen Zeitspanne über die vom Sollwert abgewichen werden darf (Δ …). Der timer x erhält einen neuen Wert, wenn der Sollwert erreicht wird. Dadurch, daß dieser timer x als ein maximaler timer (MaxTimer) bezeichnet wird, ist ausgesagt, daß nach Verlassen des Sollwertes innerhalb der Zeit Δ … der Sollwert wieder erreicht wird. Siehe Abbildung 4 auf Seite 9 zur genauen Definition von VTimer und MaxTimer. Zur übersichtlicheren Beschreibung der Hauptspezifikation spec, werden die actions zur Veränderuung der Sollwerte konjugiert. Die Definition spec besagt, daß nach der Initialiesierung nur gemäß der oben genannten Definitionen Veränderungen an den Zustandsvariablen geschehen können.

3.6 Modul Kultivierung

Im Abschnitt parameters des Moduls Kultivierung in Abbildung 5 auf Seite 9, bezeichnet die Konstante AktiveZellen_{max} die Anzahl an Zellen, die durch die Kultivierung erreicht werden sollen, um den Prozeß zu beenden und die Kultur zu ernten. Die Konstante Δ_{doppel} entspricht der Vedoppelungszeit der Tierzellen. Die Variable letzte steht für die zuletzt nach einer Verdoppelung erreichte Anzahl an lebenden Zellen im Kultumedium. Alle an der Kultivierung beteiligten Module werden eingebunden. Hat sich die Anzahl an lebenden Zellen verdoppelt, so diese der Variablen letzte zugewiesen. Somit ist die verdoppelung die einzige Möglichkeit, um letzte zu verändern. Das ziel des artifact Bioreaktor ist es, innerhalb der Verdoppelungszeit eine Verdoppelung der Kultur zu erreichen, bis die gewünschte Anzahl an Zellen vorhanden ist. Sollte eine Verunreinigung mit Bakterien stattfinden, so muß der Vorgang abgebrochen und der Bioreaktor entleert werden. Entsprechend der zuvor im Modul Kontrolle beschriebenen Vorgehensweise, wird mittels der timer VTimer und MaxTimer, welche sich auf die Veränderung der Variablen letzte beziehen, ausgedrückt, daß sich in der Zeit Δ_{doppel} die Menge an Zellen verdoppelt. Der Ausdruck

module Kontrolle Teil 2

actions pH soll(s) =^{Δ} ∧ 0 ≤ s ≤ 14 ∧ pH^{s}′ = s ∧ unchanged ⟨pO_{2}, pH , pO_{2}^{s}, temp^{s}, drehz^{s}, mDruck^{s}, mFluss^{s}, kDruck^{s}, kFluss^{s} ⟩

⋮

kFluss soll(s) =^{Δ} ∧ 0 ≤ s ∧ kFluss^{s}′ = s ∧ unchanged ⟨pO_{2}, pH , pO_{2}^{s}, temp^{s}, drehz^{s}, mDruck^{s}, mFluss^{s}, kDruck^{s} ⟩

pH korrektur =^{Δ} ∧ pH ≠ pH^{s} ∧ ∃ co, o, n, l : reaktor.mGas(co, o, n, l) ∧ ∃ w : reaktor.kGas(w) ∧ pH′ = pH^{s} ∧ unchanged ⟨pO_{2}, pO_{2}^{s}, temp^{s}, drehz^{s}, mDruck^{s}, mFluss^{s}, kDruck^{s}, kFluss^{s} ⟩

pO_{2} korrektur =^{Δ} ∧ pO_{2} ≠ pO_{2}^{s} ∧ ∃ co, o, n, l : reaktor.mGas(co, o, n, l) ∧ ∃ w : reaktor.kGas(w) ∧ pO′_{2} = pO_{2}^{s} ∧ unchanged ⟨pH , pO_{2}^{s}, temp^{s}, drehz^{s}, mDruck^{s}, mFluss^{s}, kDruck^{s}, kFluss^{s} ⟩

Tabelle 2: Modul Kontrolle, 2. Teil

□[(\begin{matrix}∨ aktiveZellen ≥ AktiveZellen_{max} \\ ∨ bakterien ≠ 0) ⇒ (\begin{matrix}∧ ∃ m, a, t : bioreaktor.entnahme(a, t, m) \\ ∧ volumen′ = 0)]_{volumen} \end{matrix} \end{matrix}

beschreibt, daß immer nach erreichen der gewünschten Zellenanzahl oder nach einer Verunreinigung das Kulturmedium restlos entnommen wird. Unter der Bezeichnung spec werden nun die einzlenen Spezifikationen der Module mit dem ziel konjugiert und bilden so die Gesamtspezifikation des Kultivierungsprozesses im Bioreaktor.

4 Warum TLA+?

Der entscheidende Vorteil von TLA^{+} ist, daß es sich um eine Sprache handelt, die auf einer Logik (TLA) basiert. Zu dieser Logik gehören logische Schlußregeln, anhand derer Aussagen miteinander verknüpft und Schlüsse gezogen werden können. Mittels dieser Schlußregeln ist es beispielsweise möglich einen logischen Beweis zu führen, daß eine implementationsnähere Spezifikation eine abstrakte Spezifikation eines Programms implementiert. Bei der hier vorliegenden Spezifikation handelt es sich nicht um ein Progamm, sondern um ein technisches Gerät. Natürlich könnten auch hier auf unterschiedlichen Abstraktionsebenen verschiedene Spezifikationen mittels Implementationsbeweisen verifiziert werden. Zusätzlich bietet sich aber auch die Möglichkeit, einen veränderten Aufbau oder zusätzliche Komponenten des Bioreaktors mit der vorhandenen Spezifikation zu verbinden und ihre Zulässigkeit logischerweise zu beweisen. Beschreibe das Modul Erweiterung die Erweiterung des vorhandenen Aufbaus und sei das Modul KultivierungNeu die neue Gesamtspezifikation mit dieser Erweiterung, so könnte mittels der Aussage :

∃ ∃ ∃ ∃ ∃ ∃ x_{1}, ⋯, x_{n} : KultivierungNeu.spec(x_{1}, ⋯, x_{n}, z_{1}, ⋯ z_{j} ) ⇒ ∃ ∃ ∃ ∃ ∃ ∃ y_{1}, ⋯, y_{m} : Kultivierung.spec(y_{1}, ⋯, y_{m}, F_{1}(z_{1}, ⋯ z_{j} ), ⋯, F_{k}(z_{1}, ⋯ z_{j} ))

(wobei die F_{i} eine bestimmte Funktion, das sogenannte ”refinement mapping“, ist) bewiesen werden, daß trotz der Erweiterung die veränderte Anlage immer noch den Anforderungen der alten Anlage entspricht. Man erkennt, daß die logische Aussage A ⇒ B, die Bedeutung hat, A implementiert B. Entsprechend den Anforderungen, unter denen ein solcher Beweis geführt werden soll, ist es

module Kontrolle Teil 3

temporal pH richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, pH korrektur, Δ_{pH} , pH ) ∧ MaxTimer(x)

pO_{2} richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, pO_{2} korrektur, Δ_{pO_{2}} , pO_{2}) ∧ MaxTimer(x)

temp richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, reaktor.heizen(temp^{s}), Δ_{temp} , temperatur) ∧ MaxTimer(x)

⋮

kFluss richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, reaktor.kFluss(kFluss^{s}), Δ_{kFluss} , kopfraumfluss) ∧ MaxTimer(x)

actions =^{Δ} ∨ ∃ s : pH soll(s) ⋮ ∨ ∃ s : kFluss soll(s)

spec =^{Δ} ∧ Init ; ∧ pH richtig ⋮ ∧ kFluss richtig ∧ □[actions]_{sollVars}

Tabelle 3: Modul Kontrolle, 3. Teil

auch möglich nur Teile der Gerätespezifikation einem solchen Beweis zu unterziehen. Entscheidend ist, daß durch die logische Beweisführung, die Umsetzung der gewünschten Veränderungen auf ihre Richtigkeit verifiziert werden kann.

5 Zusammenfassung und Ausblick

Trotz der nur vagen Beschreibung der unterschiedlichen Komponenten des Bioreaktors, ist es gelungen eine inhaltlich zutreffende und formal korrekte^{5} TLA^{+} Spezifikation zu schreiben. Dabei konnte auf dem Abstraktionsniveau des den Reaktor benutzenden Biologen verblieben werden. Alle technischen Komponenten werden nur so detailliert beschreibenden, wie es erforderlich ist, um auf einer Abstraktionsstufe mit dem Nutzen des Bioreaktors zu stehen. Hierdurch ist es möglich, auch der aktuellen philosophischen Grundlagenforschung zum Thema formale Beschreibungen, welche unter anderem von Searle [Sea96] und Ladkin [Lad96] in der Behandlung der artifacts stattfindet, gerecht zu werden. Es wurde sowohl das Zusammenspiel der Umwelt mit dem Kulturmedium, als auch die den Prozeß bestimmenden Echtzeitbedingungen berücksichtitg. Auf diesem Ergebnis aufbauend, ist es nun möglich Veränderungen, welche am Bioreaktor oder einer seiner Komponenten vorgenommen werden, mittels Korrektheisbeweise zu überprüfen. Dabei kann auf Grund der Modulsruktur nur ein begrenzter Teil als auch die gesamte Anlage in die Überprüfung mit einbezogen werden. Neu ist dabei, daß nicht die technischen Anordnungen miteinander verglichen werden, sondern daß die Veränderungen mit den im Modul Kultivierung durch spec beschriebenen Anforderungen übereinstimmen. Dies gewährleistet, daß der veränderte Aufbau weiterhin dem artifact Bioreaktor entspricht, und somit auf einer abstrakten Bedeutungsebene keine ungewollte Veränderung stattgefunden hat. Solche Beweise sind zur Zeit zwar noch sehr langwierig und arbeitsintensiv [Lad95], könnten jedoch durch eine entsprechende Untersützung von automatischen Beweisern und ”proofchecker“ vereinfacht werden.

5”formal korrekt“ bedeutet hier, daß ausschliesslich TLA^{+} Sprachelemente verwendet wurden und somit eine klare Zuordnung von Syntax und Semantik für die gesamte Spezifikation sichergestellt ist.

module Echtzeit (Ausschnitt)

parameters now : variable ∞ : constant

VTimer(x, A, δ, v) =^{Δ} ∧ x = if Enabled ⟨A⟩_{v} then now + δ else ∞ ∧ □[x′ = if ( Enabled ⟨A⟩_{v})′ then if ⟨A⟩_{v} then now′ + δ else x else ∞ ]_{⟨x,v ⟩}

MaxTimer(x) =^{Δ} □[(x ≠ ∞) ⇒ (now′ ≤ x)]_{now}

Tabelle 4: Modul Echtzeit (Ausschnitt), Die timer

module Kultivierung

parameters bakterien, letzte : Nat^{0^{+}} variable volumen : Real^{0^{+}} variable AktiveZellen_{max} , Δ_{doppel} : constant

import MiscDef import Echtzeit include Umgebung as umgebung include Medium as medium include Bioreaktor as bioreaktor include Kontrolle as kontrolle

predicates Init =^{Δ} letzte = 0

actions verdoppelung =^{Δ} ∧ aktiveZellen ≥ 2 · letzte ∧ letzte′ = aktiveZellen ∧ unchanged ⟨bakterien, volumen ⟩

temporal ziel =^{Δ} ∧ ∃ ∃ ∃ ∃ ∃ ∃ x : Vtimer(x, verdoppelung, Δ_{doppel} , letzte) ∧ MaxTimer(x) ∧ □[(\begin{matrix}∨ aktiveZellen ≥ AktiveZellen_{max} \\ ∨ bakterien ≠ 0) ⇒ (\begin{matrix}∧ ∃ m, a, t : bioreaktor.entnahme(a, t, m) \\ ∧ volumen′ = 0)]_{volumen} \end{matrix} \end{matrix}

spec =^{Δ} ∧ Init ∧ umgebung.spec ∧ medium.spec ∧ bioreaktor.spec ∧ kontrolle.spec ∧ ziel

Tabelle 5: Modul Kultivierung

Literatur

[ABL96] Jean-Raymond Abrial, Egon Börger, Hans Langmaack: editors. Formal Methods for Industrial Applications – Specifying and Programming the Steam Boiler Control. Lecture Notes in Computer Science, Vol. 1165, Springer Verlag, 1996.

[AL94] Martín Abadi, Leslie Lamport. An Old-Fashioned Recipe for Real Time. ACM Transactions on Programming Languages and Systems, 16(5):1543-1571, September 1994.

[Lad95] Peter Ladkin. Formal But Lively Buffers in TLA^{+} . Technical Report 96-07 der Technischen Fakultät, Arbeitsgruppe RVS, Universität Bielefeld.

Available from http://www.rvs.uni-bielefeld.de.

[Lad96] Peter Ladkin. The Success and Failure of Artifacts. Technical Report RVS-Occ-97-04 der Technischen Fakultät, Arbeitsgruppe RVS, Universität Bielefeld. Available from

http://www.rvs.uni-bielefeld.de.

[Lam93] Leslie Lamport. Hybrid Systems in TLA^{+} . Grossmann, Nerode, Ravn, Rischl: editors. Hybrid Systems, Lecture Notes in Computer Science, Vol. 736. Springer Verlag, 1993.

[Lam94] Leslie Lamport. The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, Mai 1994.

[Lam95] Leslie Lamport. TLA^{+} .

Available from http://www.research.digital.com/SRC/tla/.

[Lüt93] Dirk Lütkemeyer. Mikroporöse Membranionenaustauscher zur schnellen Reinigung von Proteinen aus tierischen Zellkulturen. Dissertation an der Technischen Fakultät der Univeristät Bielefeld, Juli 1993.

[Pirt75] S. John Pirt. Principles of Microbe and Cell Cultivation. Oxford: Blackwell Scientific Publications, 1975.

[Sea96] John R. Searle. The Construction of Social Reality. London: Penguin Books, 1996.

[SL97] Lutz Sommerfeld, Peter Ladkin.

Beschreibung eines vagen Echtzeit-Hybrid-Systems in TLA^{+} .

Available from http://www.rvs.uni-bielefeld.de/~lutz/.

A Die Module

Bei den Modulen in diesem Anhang handelt es sich um vorläufige Ergebnisse. Kleinere Veränderungen sind daher nicht auszuschließen.

A.1 Echtzeit

module Echtzeit

parameters now : variable ∞ : constant

import MiscDef

assumption InfinityUnReal =^{Δ} ∞ ∉ Real

actions RT (v) =^{Δ} ∧ now ∈ Real ∧ □[\begin{matrix}∧ now′ ∈ \{r ∈ Real : r > now\} \\ ∧ v′ = v]_{now} \end{matrix} ∧ ∀ t ∈ Real : ◇(now > t)

VTimer(x, A, δ, v) =^{Δ} ∧ x = if Enabled ⟨A⟩_{v} then now + δ else ∞ ∧ □[x′ = if ( Enabled ⟨A⟩_{v})′ then if ⟨A⟩_{v} then now′ + δ else x else ∞ ]_{⟨x,v ⟩}

MaxTimer(x) =^{Δ} □[(x ≠ ∞) ⇒ (now′ ≤ x)]_{now} kontinuierlich(v) =^{Δ} ∀ i ∈ 1..Len(v) : □[∀ δ ∈ Real^{+} : ∃ ϵ ∈ Real : now′ − now < ϵ ⇒ |v[i]′ − v[i]| < δ]_{v[i]}

A.2 MiscDef

module MiscDef

import Reals import Naturals import Sequences^{6}

definitions Real^{+} =^{Δ} {x ∈ Real : x > 0} Real^{0^{+}} =^{Δ} {x ∈ Real : x ≥ 0} Nat^{+} =^{Δ} {n ∈ Nat : n > 0} Nat^{0^{+}} =^{Δ} {n ∈ Nat : n ≥ 0} |z| =^{Δ} if z < 0 then −z else z

6from Peter Ladkin

A.3 Umgebung

module Umgebung

parameters temperatur, helligkeit : variable Temperatur_{0}, Helligkeit_{0}, MaxHelligkeit : constant

predicates Init =^{Δ} ∧ temperatur = Temperatur_{0} ∧ helligkeit = Helligkeit_{0}

definitions tempBed =^{Δ} 10^{∘}C ≤ temperatur′ ≤ 35^{∘}C lichtBed =^{Δ} helligkeit′ ≤ MaxHelligkeit

temporal vars =^{Δ} ⟨temperatur, helligkeit ⟩ spec =^{Δ} ∧ Init ∧ □[tempBed ∧ lichtBed]_{vars} ∧ RT (vars) ∧ kontinuierlich(vars)

A.4 Medium

module Medium

parameters aktiveZellen, toteZellen, bakterien : Nat^{0^{+}} variable pH , pO_{2}, temperatur, raumtemperatur : Real^{+} variable basalmedium : Zutaten ∪ Gifte → Real^{0^{+}} variable Zutaten, Gifte, Basalmedium_{0}, pH_{0}, pO_{2}_{(0)}, temperatur_{0} : constant AktiveZellen_{0}, ToteZellen_{0} : constant

import Echtzeit include Umgebung as umwelt with raumtemperatur ← temperatur

predicates Init =^{Δ} ∧ aktiveZellen = AktiveZellen_{0} ∧ toteZellen = ToteZellen_{0} ∧ basalmedium = Basalmedium_{0} ∧ pH = pH_{0} ∧ pO_{2} = pO_{2}_{(0)} ∧ temperatur = temperatur_{0} ∧ bakterien = 0

actions wachstum =^{Δ} ∧ aktiveZellen′ = aktiveZellen + 1 ∧ unchanged ⟨\begin{matrix}raumtemperatur, toteZellen, basalmedium, pH , pO_{2}, \\ temperatur, bakterien ⟩ \end{matrix} sterben =^{Δ} ∧ aktiveZellen > 0 ∧ aktiveZellen′ = aktiveZellen − 1 ∧ toteZellen′ = toteZellen + 1 ∧ unchanged ⟨raumtemperatur, basalmedium, pH , pO_{2}, temperatur, bakterien ⟩ verbrauch =^{Δ} ∧ ∃ z ∈ Zutaten : 0 ≤ basalmedium′[z] < basalmedium[z] ∧ ∀ x ∈ Zutaten ∪ Gifte : (x = z ∨ unchanged basalmedium[x]) ∧ unchanged ⟨\begin{matrix}raumtemperatur, aktiveZellen, toteZellen, \\ pH , pO_{2}, temperatur, bakterien ⟩ \end{matrix} ausscheidung =^{Δ} ∧ ∃ g ∈ Gifte : basalmedium′[g] > basalmedium[g] ∧ ∀ x ∈ Zutaten ∪ Gifte : (x = g ∨ unchanged basalmedium[x]) ∧ unchanged ⟨\begin{matrix}raumtemperatur, aktiveZellen, toteZellen, \\ pH , pO_{2}, temperatur, bakterien ⟩ \end{matrix} pHaenderung =^{Δ} ∧ 0 ≤ pH′ ≤ 14 ∧ pH′ ≠ pH ∧ unchanged ⟨\begin{matrix}raumtemperatur, aktiveZellen, toteZellen, basalmedium, \\ pO_{2}, temperatur, bakterien ⟩ \end{matrix} pO_{2}aenderung =^{Δ} ∧ 0 ≤ pO′_{2} ≤ 500 ∧ pO′_{2} ≠ pO_{2} ∧ unchanged ⟨\begin{matrix}raumtemperatur, aktiveZellen, toteZellen, basalmedium, \\ pH , temperatur, bakterien ⟩ \end{matrix} abkuehlung =^{Δ} ∧ raumtemperatur ≤ temperatur′ < temperatur ∧ unchanged ⟨\begin{matrix}raumtemperatur, aktiveZellen, toteZellen, \\ basalmedium, pH , pO_{2}, bakterien ⟩ \end{matrix}

temporal vars1 =^{Δ} ⟨pH , pO_{2}, temperatur, raumtemperatur ⟩ vars =^{Δ} vars1 ∘ ⟨basalmedium, aktiveZellen, toteZellen, bakterien ⟩ actions =^{Δ} ∨ wachstum ∨ sterben ∨ verbrauch ∨ pHaenderung ∨ pO_{2}aenderung ∨ abkuehlung

spec =^{Δ} ∧ Init ∧ □[actions]_{vars} ∧ RT (vars) ∧ kontinuierlich(vars1)

A.5 Bioreaktor

module Bioreaktor

parameters ruehrerdrehzahl, membrandruck, membrangas, membrangasfluss : Real^{0^{+}} variable temperatur, kopfraumdruck, kopfraumgas, kopfraumgasfluss, volumen : Real^{0^{+}} variable aktiveZellen, toteZellen, bakterien : Nat^{0^{+}} variable basalmedium : Zutaten → Real^{0^{+}} variable Zutaten, Volumen_{0}, Drehzahl_{0} : constant Membrandruck_{0}, Membrangas_{0}, Membrangasfluss_{0} : constant Kopfraumdruck_{0}, Kopfraumgas_{0}, Kopfraumgasfluss_{0} : constant

import Echtzeit include Medium as medium

definitions Maxvolumen =^{Δ} 20

predicates Init =^{Δ} ∧ ruehrerdrehzahl = Drehzahl_{0} ∧ volumen = Volumen_{0} ∧ membrandruck = Membrandruck_{0} ∧ membrangas = Membrangas_{0} ∧ membrangasfluss = Membrangasfluss_{0} ∧ kopfraumdruck = Kopfraumdruck_{0} ∧ kopfraumgas = Kopfraumgas_{0} ∧ kopfraumgasfluss = Kopfraumgasfluss_{0}

actions neueZellen(a, t) =^{Δ} ∧ a ∈ Nat^{+} ∧ t ∈ Nat^{0^{+}} ∧ aktiveZellen′ = aktiveZellen + a ∧ toteZellen′ = toteZellen + t ∧ volumen < volumen′ ≤ Maxvolumen ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangas, membrangasfluss, kopfraumgas, \\ kopfraumgasfluss, basalmedium, temperatur, bakterien ⟩ \end{matrix}

neuesMedium(m) =^{Δ} ∧ m ∈ Zutaten → Real^{0^{+}} ∧ ∀ x ∈ Zutaten : basalmedium[x]′ = basalmedium[x] + m[x] ∧ volumen < volumen′ ≤ Maxvolumen ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangas, membrangasfluss, kopfraumgas, \\ kopfraumgasfluss, aktiveZellen, toteZellen, \\ temperatur, bakterien ⟩ \end{matrix}

entnahme(a, t, m) =^{Δ} ∧ t, a ∈ Nat^{0^{+}} ∧ a ≤ aktiveZellen ∧ t ≤ toteZellen ∧ m ∈ Zutaten → Real^{+} ∧ aktiveZellen′ = aktiveZellen − a ∧ toteZellen′ = toteZellen − t ∧ ∀ x ∈ Zutaten : ∧ basalmedium[x]′ = basalmedium[x] − m[x] ∧ 0 ≤ basalmedium[x]′ ∧ 0 ≤ volumen′ < volumen ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangas, membrangasfluss, kopfraumgas, \\ kopfraumgasfluss, temperatur, bakterien ⟩ \end{matrix} verseuchung(n) =^{Δ} ∧ n ∈ Nat^{+} ∧ bakterien′ = bakterien + n ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangas, membrangasfluss, kopfraumgas, \\ kopfraumgasfluss, aktiveZellen, toteZellen, \\ basalmedium, temperatur, volumen ⟩ \end{matrix} heizen(t) =^{Δ} ∧ t > temperatur ∧ temperatur′ = t ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangas, membrangasfluss, kopfraumgas, \\ kopfraumgasfluss, aktiveZellen, toteZellen, \\ basalmedium, bakterien, volumen ⟩ \end{matrix} drehzahl(d) =^{Δ} ∧ d ∈ Real^{0^{+}} ∧ d ≠ ruehrerdrehzahl ∧ ruehrerdrehzahl′ = d ∧ unchanged ⟨\begin{matrix}kopfraumdruck, membrandruck, membrangas, \\ membrangasfluss, kopfraumgas, kopfraumgasfluss, \\ aktiveZellen, toteZellen, basalmedium, \\ temperatur, bakterien, volumen ⟩ \end{matrix} mGas(co, o, n, l) =^{Δ} ∧ co, o, n, l ∈ Real^{0^{+}} ∧ co + o + n + l = 100 ∧ ⟨co, o, n, l ⟩ ≠ membrangas ∧ membrangas′ = ⟨co, o, n, l ⟩ ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangasfluss, kopfraumgasfluss, aktiveZellen, \\ toteZellen, basalmedium, temperatur, \\ bakterien, volumen, kopfraumgas ⟩ \end{matrix} kGas(wahl) =^{Δ} ∧ wahl ∈ \{“luft”, “gemisch”\} ∧ kopfraumgas′ = if wahl = “luft” then ⟨0, 0, 0, 100⟩ else membrangas ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangasfluss, kopfraumgasfluss, aktiveZellen, \\ toteZellen, basalmedium, temperatur, \\ bakterien, volumen, membrangas ⟩ \end{matrix} mFluss(m) =^{Δ} ∧ m ∈ Real^{0^{+}} ∧ m ≠ membrangasfluss ∧ membrangasfluss′ = m ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangas, kopfraumgas, aktiveZellen, toteZellen, \\ basalmedium, temperatur, bakterien, volumen, \\ kopfraumgasfluss ⟩ \end{matrix} kFluss(m) =^{Δ} ∧ m ∈ Real^{0^{+}} ∧ m ≠ kopfraumgasfluss ∧ kopfraumgasfluss′ = m ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, \\ membrangas, kopfraumgas, aktiveZellen, toteZellen, \\ basalmedium, temperatur, bakterien, volumen, \\ membrangasfluss ⟩ \end{matrix} mDruck(d) =^{Δ} ∧ d ∈ Real^{+} ∧ d ≠ membrandruck ∧ membrandruck′ = d ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, membrangas, membrangasfluss, \\ kopfraumgas, kopfraumgasfluss, kopfraumdruck, \\ aktiveZellen, toteZellen, basalmedium, \\ temperatur, bakterien, volumen ⟩ \end{matrix}

kDruck(d) =^{Δ} ∧ d ∈ Real^{+} ∧ d ≠ kopfraumdruck ∧ kopfraumdruck′ = d ∧ unchanged ⟨\begin{matrix}ruehrerdrehzahl, membrangas, membrangasfluss, \\ kopfraumgas, kopfraumgasfluss, membrandruck \\ aktiveZellen, toteZellen, basalmedium, \\ temperatur, bakterien, volumen ⟩ \end{matrix}

temporal vars1 =^{Δ} ⟨\begin{matrix}ruehrerdrehzahl, kopfraumdruck, membrandruck, membrangas, membrangasfluss, \\ kopfraumgas, kopfraumgasfluss, temperatur, volumen ⟩ \end{matrix}

vars =^{Δ} vars1 ∘ ⟨basalmedium, aktiveZellen, toteZellen, bakterien ⟩ actions =^{Δ} ∨ ∃ a, t : neueZellen(a, t) ∨ ∃ m : neuesMedium(m) ∨ ∃ a, t, m : entnahme(a, t, m) ∨ ∃ n : verseuchung(n)

spec =^{Δ} ∧ Init ∧ □[actions]_{vars} ∧ RT (vars) ∧ kontinuierlich(vars1)

A.6 Kontrolle

module Kontrolle

parameters pH , pO_{2}, temperatur, ruehrerdrehzahl : Real^{0^{+}} variable membrandruck, membrangasfluss : Real^{0^{+}}variable kopfraumdruck, kopfraumgasfluss : Real^{0^{+}}variable pH^{s}, pO_{2}^{s}, temp^{s}, drehz^{s}, mDruck^{s}, mFluss^{s}, kDruck^{s}, kFluss^{s} : variable Δ_{pH} , Δ_{pO_{2}}, Δ_{temp}, Δ_{drehz} , Δ_{mDruck}, Δ_{kDruck}, Δ_{mFluss}, Δ_{kFluss} : constant pH _{0}^{s}, pO_{2}_{(0)}^{s}, temp_{0}^{s}, drehz_{0}^{s}, mDruck_{0}^{s}, mFluss_{0}^{s}, kDruck_{0}^{s}, kFluss_{0}^{s} : constant

definitions sollVars =^{Δ} ⟨pH^{s}, pO_{2}^{s}, temp^{s}, drehz^{s}, mDruck^{s}, mFluss^{s}, kDruck^{s}, kFluss^{s} ⟩

import Echtzeit include Bioreaktor as reaktor

predicates

Init =^{Δ} ∧ pH^{s} = pH _{0}^{s} ∧ pO_{2}^{s} = pO_{2}_{(0)}^{s} ∧ temp^{s} = temp_{0}^{s} ∧ drehz^{s} = drehz_{0}^{s} ∧ mDruck^{s} = mDruck_{0}^{s} ∧ mFluss^{s} = mFluss_{0}^{s} ∧ kDruck^{s} = kDruck_{0}^{s} ∧ kFluss^{s} = kFluss_{0}^{s}

actions pH soll(s) =^{Δ} \begin{matrix}∧ 0 ≤ s ≤ 14 \\ ∧ pH^{s}′ = s \end{matrix} pO_{2} soll(s) =^{Δ} \begin{matrix}∧ 0 ≤ s ≤ 100 \\ ∧ pO_{2}^{s}′ = s \end{matrix} temp soll(s) =^{Δ} \begin{matrix}∧ 10 ≤ s ≤ 80 \\ ∧ temp^{s}′ = s \end{matrix} drehz soll(s) =^{Δ} ∧ 0 ≤ s ≤ 50 ; ∧ drehz^{s}′ = s mDruck soll(s) =^{Δ} ∧ 0 ≤ s ∧ mDruck^{s}′ = s kDruck soll(s) =^{Δ} ∧ 0 ≤ s ∧ kDruckd^{s}′ = s mFluss soll(s) =^{Δ} ∧ 0 ≤ s ∧ mFluss^{s}′ = s kFluss soll(s) =^{Δ} ∧ 0 ≤ s ∧ kFluss^{s}′ = s pH korrektur =^{Δ} ∧ pH ≠ pH^{s} ∧ ∃ co, o, n, l : reaktor.mGas(co, o, n, l) ∧ ∃ w : reaktor.kGas(w) ∧ pH′ = pH^{s} ∧ unchanged pO_{2}

pO_{2} korrektur =^{Δ} ∧ pO_{2} ≠ pO_{2}^{s} ∧ ∃ co, o, n, l : reaktor.mGas(co, o, n, l) ∧ ∃ w : reaktor.kGas(w) ∧ pO′_{2} = pO_{2}^{s} ∧ unchanged pH

temporal pH richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, pH korrektur, Δ_{pH} , pH ) ∧ MaxTimer(x) pO_{2} richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, pO_{2} korrektur, Δ_{pO_{2}}, pO_{2}) ∧ MaxTimer(x) temp richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, reaktor.heizen(temp^{s}), Δ_{temp}, temperatur) ∧ MaxTimer(x) drehz richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, reaktor.drehzahl(drehz^{s}), Δ_{drehz} , ruehrerdrehzahl) ∧ MaxTimer(x) mDruck richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, reaktor.mDruck(mDruck^{s}), Δ_{mDruck}, membrandruck) ∧ MaxTimer(x) kDruck richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, reaktor.kDruck(kDruckd^{s}), Δ_{kDruck}, kopfraumdruck) ∧ MaxTimer(x) mFluss richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, reaktor.mFluss(mFluss^{s}), Δ_{mFluss}, membranfluss) ∧ MaxTimer(x)

kFluss richtig =^{Δ} ∃ ∃ ∃ ∃ ∃ ∃ x : ∧ VTimer(x, reaktor.kFluss(kFluss^{s}), Δ_{kFluss}, kopfraumfluss) ∧ MaxTimer(x)

actions =^{Δ} ∨ ∃ s : pH soll(s) ∨ ∃ s : pO_{2} soll(s) ∨ ∃ s : temp soll(s) ∨ ∃ s : drehz soll(s) ∨ ∃ s : mDruck soll(s) ∨ ∃ s : kDruck soll(s) ∨ ∃ s : mFluss soll(s) ∨ ∃ s : kFluss soll(s)

spec =^{Δ} ∧ Init ∧ pH richtig ∧ pO_{2} richtig ∧ temp richtig ∧ drehz richtig ∧ mDruck richtig ∧ kDruck richtig ∧ mFluss richtig ∧ kFluss richtig ∧ □[actions]_{sollVars}

A.7 Kultivierung

module Kultivierung

parameters bakterien, letzte : Nat^{0^{+}} variable volumen : Real^{0^{+}} variable AktiveZellen_{max} , Δ_{doppel} : constant

import MiscDef import Echtzeit include Umgebung as umgebung include Medium as medium include Bioreaktor as bioreaktor include Kontrolle as kontrolle

predicates Init =^{Δ} letzte = 0

actions verdoppelung =^{Δ} ∧ aktiveZellen ≥ 2 · letzte ∧ letzte′ = aktiveZellen ∧ unchanged ⟨bakterien, volumen ⟩

temporal ziel =^{Δ} ∧ ∃ ∃ ∃ ∃ ∃ ∃ x : Vtimer(x, verdoppelung, Δ_{doppel}, letzte) ∧ MaxTimer(x) ∧ □[(\begin{matrix}∨ aktiveZellen ≥ AktiveZellen_{max} \\ ∨ bakterien ≠ 0) ⇒ (\begin{matrix}∧ ∃ m, a, t : bioreaktor.entnahme(a, t, m) \\ ∧ volumen′ = 0)]_{volumen} \end{matrix} \end{matrix} spec =^{Δ} ∧ Init ∧ umgebung.spec ∧ medium.spec ∧ bioreaktor.spec ∧ kontrolle.spec