Ph.D.
Eine Methode zur formalen Modellierung von Betriebssystemkonzepten
Author(s): Katharina Spies
Year: 1998
Publisher: TUM-I9809
Editor:
CR Classification: D.2.1, D.3.1, D.4.0, D.4.1, D.4.2, D.4.4, F.3.1
CR General Terms: Design, Theory, Languages
Keywords: Focus, formale Methode, Spezifikation, Modellierung, Betriebssysteme, dynamische Systeme, inkrementelle Spezifikationsentwicklung
Abstract:Focus umfaßt allgemeine Konzepte, Beschreibungs- und Verfeinerungstechniken zur
Top-Down-Entwicklung verteilter, reaktiver Systeme. Betriebssysteme sind
langlebige Softwareprodukte, die von größter Wichtigkeit und für die Nutzung
von Rechensystemen unverzichtbar sind. Die systematische Entwicklung von
Betriebssystemen mit formalen Verfahren wurde bisher nur wenig betrachtet und
ist für den Einsatz von Focus eine Herausforderung. Die vorliegende Arbeit
zeigt, daß 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 Kernfunktionalität zu modellieren und zu diesen schrittweise weitere
Funktionalitäten hinzuzunehmen, wobei bereits erstellte Spezifikationen
konsequent erweitert, angepaßt und weiterentwickelt werden. Die methodische
Entwicklung der Betriebsystemspezifikation basiert auf einem Kernsystem zur
Modellierung von Konzepten der Prozessorverwaltung. Dieses wird schrittweise
erweitert um Konzepte der Speicherverwaltung, Prozeßkooperation sowie die
Erzeugung von Prozessen. Das Ergebnis ist ein in Focus modelliertes
Betriebssystem, mit dem wesentlichen Teile der Ressourcenverwaltung auf hohem
Abstraktionsniveau beschrieben sind. Aufgrund der systematischen Vorgehensweise
kann die vollständige Modellierung in kleinen, an speziellen
Betriebssystemaufgaben orientierten Schritten nachvollzogen werden.
Available as compressed Postscript
BibTeX-Entry:
<![CDATA[
@phdthesis{SpiesK98,
author = {Katharina Spies},
title = {Eine Methode zur formalen Modellierung von Betriebssystemkonzepten},
type = {PHDrep},
school = {Technische Univerit\"at M\"unchen},
year = {1998},
url = {http://www4.informatik.tu-muenchen.de/reports/SpiesK98.html},
abstract = {Focus umfaßt allgemeine Konzepte, Beschreibungs- und Verfeinerungstechniken zur
Top-Down-Entwicklung verteilter, reaktiver Systeme. Betriebssysteme sind
langlebige Softwareprodukte, die von größter Wichtigkeit und für die Nutzung
von Rechensystemen unverzichtbar sind. Die systematische Entwicklung von
Betriebssystemen mit formalen Verfahren wurde bisher nur wenig betrachtet und
ist für den Einsatz von Focus eine Herausforderung. Die vorliegende Arbeit
zeigt, daß 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 Kernfunktionalität zu modellieren und zu diesen schrittweise weitere
Funktionalitäten hinzuzunehmen, wobei bereits erstellte Spezifikationen
konsequent erweitert, angepaßt und weiterentwickelt werden. Die methodische
Entwicklung der Betriebsystemspezifikation basiert auf einem Kernsystem zur
Modellierung von Konzepten der Prozessorverwaltung. Dieses wird schrittweise
erweitert um Konzepte der Speicherverwaltung, Prozeßkooperation sowie die
Erzeugung von Prozessen. Das Ergebnis ist ein in Focus modelliertes
Betriebssystem, mit dem wesentlichen Teile der Ressourcenverwaltung auf hohem
Abstraktionsniveau beschrieben sind. Aufgrund der systematischen Vorgehensweise
kann die vollständige Modellierung in kleinen, an speziellen
Betriebssystemaufgaben orientierten Schritten nachvollzogen werden.},
CRClassification = {D.2.1, D.3.1, D.4.0, D.4.1, D.4.2, D.4.4, F.3.1},
CRGenTerms = {Design, Theory, Languages}}
]]>