Softwareentwicklung auf ressourcenbeschränkten Mikrorechnern verläuft meist eindimensional: es wird modularer C-Code für eine Zielplattform mit dem zugehörigen Compiler in eine ausführbare Datei übersetzt, auf das Ziel geschrieben und dort in der Ausführung validiert. Die Validierung erfolgt in der Sprache des Programmiermodells, der Ziel- zustand und seine Evolution ist letztendlich ein Blockdatensatz. Der Befehlszeiger deutet auf den Auslöser des aktuellen Evolu-tionsschritts in diesem Blocksatz. Damit kann das Programmiermodell ein lineares genannt werden; zur Validierung müssen geeignete Darstellungen für diesen Blocksatz gefunden werden, sowohl zeitlokal als auch dynamisch. Insbesondere müssen Korrelationen zwischen diesen Unterblöcken einfach darstellbar sein. Zur Falsifizierung und Verifikation muss der Blocksatz manipulierbar und seine Ausführung (Dynamik) steuerbar sein. Diese Arbeit mit Blocksatzdaten kann mit elementaren Algorithmen auch in einer Textkonsole oder einem leistungsfähigen Editor wie Emacs stattfinden.
展开▼
