Abstract: In dieser Arbeit wird mit Hilfe formaler Methoden (Fehlerbaumbasierte Bedrohungsanalyse, Ableitung von Sicherheitsbedingungen und -mechanismen, CSP-Spezifikation, Verifikation von Sicherheitseigenschaften durch Modelchecking) eine Sicherheitsschicht für einen sensorikbestückten elektrischen Rollstuhl entwickelt. Diese garantiert durch die konsequente Berücksichtigung von Worst-Case-Betrachtungen mit Hilfe neuartiger virtueller Sensoren eine kollisionsfreie Navigation in einer geeigneten Umgebung. Zusätzlich ermöglicht sie über ein realzeitfähiges Netzwerkprotokoll die Integration unterschiedlicher Rechner und Betriebssysteme. Damit lassen sich sowohl zeitkritische als auch nichtrealzeitfähige Applikationen in einem System gemeinsam betreiben. Der entwickelte Verifikationsansatz, der auf der Idee basiert, die Spezifikation des Systems gegen eine CSP-Implementierung des Fehlerbaums zu überprüfen, um zu garantieren, daß das System niemals einen katastrophalen Zustand annimmt, ist hinreichend abstrakt beschrieben, um auf andere Anwendungsgebiete übertragen zu werden.