Michaelīs Website
Michaelīs Website
Michaelīs Homepage


Diese Homepage ist im Zusammenhang mit meiner Tätigkeit in der Arbeitsgruppe von Prof. Ladkin entstanden. Wenn Fragen zu einzelnen Inhalten dieser Seite auftreten, so würde ich mich freuen, wenn Sie sich per email an mich wenden.

email: mblume@rvs.uni-bielefeld.de


Inhalt dieser Hompage


Spezifikation - und Verifikation

Die Spezifikation von Algorithmen spielt in der Informatik eine große Rolle. Zum einen liegt das daran, daß eine Spezifikation die gew"unschten Eigenschaften des Algorithmus exakt beschreibt, zum anderen kann man auf Grund der Spezifikation den Algorithmus verifizieren d.h. seine Korrektheit beweisen. Das formale Spezifizieren und Beweisen findet heute immer mehr Anwendung z.B. in sicherheitskritischen Systemen. Für diese Anwendungen sind speziell seit den 80' Jahren verschiedene Methoden entwickelt worden, bzw werden entwickelt. In jüngerer Zeit werden auch vermehrt in sich abgeschlossene Systeme genutzt, um daß Spezifizieren und Beweisen möglichst komfortabel zu gestalten. Diese Systeme werden auch unter dem Begriff "Authomatik Theoremproover" zusammengefaßt.

Die Spezifikationssprache TLA+

TLA+ ist eine Spezifikationssprache, die auf der T-emporalen L-ogik der A-ktionen basiert, die von Leslie Lamport entwickelt wurde. Die TLA-Logik ist die mathematische Grundlage für TLA+. TLA+ ist genauso mächtig wie TLA und jeder Satz in TLA+ ist in TLA übersetzbar. D.h. eine Verifikation in TLA+ ist auch ein Beweis in der formalen Logik TLA. Für diese Einleitung in TLA+ benötigt man aber keine Kenntnisse über TLA. Der Grund, warum man TLA+ anstelle der TLA benutzt liegt in den Vorteilen, die TLA+ bietet: die TLA+-Schreibweise ist unter anderem wesentlich besser zu lesen und zu schreiben. TLA+ hat auch den Vorteil, daß es eine Sprache ist und damit Syntax und Semantik besitzt. Die Kontrolle der Semantik obliegt wie immer dem ''Programmierer'' selbst; es ist aber möglich, die syntaktische Korrektheit z.B. mit Hilfe eines Parsers festzustellen. TLA+ bietet die Möglichkeit, die Spezifikation programmiersprachennah zu gestalten, da es ähnlich aufgebaut ist wie Modula3. Hierbei darf man aber nicht vergessen, daß es sich immernoch um eine Logik handelt und somit nur Zustände abgefragt werden können! Die größte Stärke von TLA+ liegt aber auf dem Gebiet der Verifikation, denn zum einen basiert sie auf einer Logik, die temporale Abläufe (siehe dazu auch meine " Einführung in die Spezifikationssprache TLA+" Abschnitt 4 Temporal- oder das Problem der ''Fairness'') berücksichtigt, und zum anderen folgen die Beweise einem sog. ''Proofscheme'' -- was eine Automatisierung ermöglicht. Es folgen nun Quellenhinweise zum Thema TLA+, in denen man evtl. Antworten auf weitere Fragen finden kann.


Informationen zu Vorlesungen von Prof. P. Ladkin


Technische Informatik I : Betriebssysteme

Die Tutoren Homepage bietet einen Überblick über die Themen der Vorlesung, so daß auf ihr neben den Aufgaben und Musterlösungen zur oben genannten Vorlesung auch noch Informationen zu zu anderen Themen zu finden sind.
Tutoren WWW-Page zur Vorlesung: Technische Informatik I : Betriebssysteme (SS 97) .

Systemadministrations Seminar und andere Seminararbeiten..

Im Zusammenhang mit dem Systemadministrations Seminar , habe ich einen Vortrag über die Ethernet-Technologie im LAN gehalten. Der komplette Foliensatz des Vortrags und die Ausarbeitung sind hier zu finden:

Im Rahmen der Vorlesung Technische Informatik I von Prof. Peter Ladkin wurde eine Einführung in die Pipelining-Technik erstellt.


Some useful things ...

Auf der Link-Page habe ich ein paar mehr oder weniger nützliche Adressen im WWW zusammen gestellt.


Frequently asked questions (FAQs)
Diese Page enthält Antworten auf Fragen - oder Problemen, mit denen wir uns beschäftigt haben und von denen wir meinen, daß sie häufiger auftreten. Falls Ihr euch auch mit Problemen herumgeschlagen habt, so teilt uns doch Eure Lösungen mit, vielleicht hilft Eure Lösung auch anderen.

FAQs

Copyright © Michael Blume
Michael Blume Last modification on 2000-04-12