Eine Methode zur formalen Modellierung von Betriebssystemkonzepten

Focus umfasst allgemeine Konzepte, Beschreibungs- und Verfeinerungstechniken zur Top-Down-Entwicklung verteilter, reaktiver Systeme. Mit seiner praezisen, formalen Basis ist Focus ueberall dort einsetzbar, wo ein System als Netz von interagierenden Komponenten modelliert werden kann. Betriebssysteme sind langlebige Softwareprodukte, die von grösster Wichtigkeit und fuer die Nutzung von Rechensystemen unverzichtbar sind. Sie sind Systeme mit einer grossen Anzahl interagierender Komponenten und bieten mit den Problemen der Ressourcenverwaltung sowie in bezug auf Strukturierung und Abstraktion eine Vielzahl interessanter Aufgabenstellungen. Die systematische Entwicklung von Betriebssystemen mit formalen Verfahren wurde bisher nur wenig betrachtet und ist fuer den Einsatz von Focus eine Herausforderung. Die vorliegende Arbeit zeigt, dass das semantische Modell von Focus dazu geeignet ist, Betriebssysteme zu modellieren. Es werden Spezifikationsmuster zur schematischen Erstellung formaler Spezifikationen definiert. Die Spezifikationserstellung orientiert sich zum einen an der systematischen und einheitlichen Darstellung der Formalisierungen. Zum anderen findet das Prinzip Verwendung, einfache Systeme mit Kernfunktionalitaet zu modellieren und zu diesem schrittweise weitere Funktionalitaeten hinzuzunehmen, wobei bereits erstellte Spezifikationen konsequent erweitert, angepasst und weiterentwickelt werden. Die methodische Vorgehensweise zur Entwicklung einer Systemspezifikation basiert auf einem Kernsystem zur Modellierung von Konzepten der Prozessorverwaltung. Das Kernsystem wird schrittweise erweitert um Konzepte der Speicherverwaltung mit virtuellem Speicher, Prozesskooperation durch Nachrichtenaustausch sowie die Erzeugung von Prozessen und deren Integration in das bestehende System. Als Ergebnis erhalten wir ein in Focus modelliertes Betriebssystem, mit dem wesentliche Teile der Ressourcenverwaltung auf hohem Abstraktionsniveau beschrieben sind. Durch den konsequenten Einsatz der Spezifikationsmuster entstehen Spezifikationen in einem einheitlichen Format. Aufgrund der systematischen Vorgehensweise kann die vollstaendige Modellierung in kleinen, an speziellen Betriebssystemaufgaben orientierten Schritten nachvollzogen werden.     «

Focus umfasst allgemeine Konzepte, Beschreibungs- und Verfeinerungstechniken zur Top-Down-Entwicklung verteilter, reaktiver Systeme. Mit seiner praezisen, formalen Basis ist Focus ueberall dort einsetzbar, wo ein System als Netz von interagierenden Komponenten modelliert werden kann. Betriebssysteme sind langlebige Softwareprodukte, die von grösster Wichtigkeit und fuer die Nutzung von Rechensystemen unverzichtbar sind. Sie sind Systeme mit einer grossen Anzahl interagierender Komponenten und bi...     »