In: Studientexte: Programmierung paralleler Prozesse, pages 50-65. TU Dresden, Weiterbildungszentrum für mathematische Kybernetik und Rechentechnik, 1987. In German.
Abstract: Das Ziel dieser Arbeit beteht darin, für eine spezielle Kommunikationssoftware die Nachweisführung ihrer Fehlerfreiheit darzustellen. - Die gegebene MKS wird in der ersten Modellierungsebene durch eine programmnahe Darstellung als ein softwareinterpretiertes Netz beschrieben. Daraus wird dann durch Verfeinerung in zwei Schritten eine programmferne, aber sehr detaillierte Darstellung in Form eines unbewerteten Petri-Netzes entwickelt.