Beschreibung eines vagen Echtzeit-Hybrid-Systems in TLA~+

摘要

Diese Spezifikation beschreibt ein technischen Gerät, für das keine physikalisch oder math-matisch 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 Spezifikations-sprache wurde TLA~+ gewählt.