 | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights | ||||||||||||||||||||||||||||||||||||||||||||||
| Wissensbrowser starten | ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||||||||||||||||||||||||||||||||||||||||||
| ||||||
|  | | | |  | |
| ||||||
| ||||||
|  | | ||||
| ||||||
Erfahrung |
|
Korrektheit per Konstruktion: Entwicklung eines sicherheitskritischen Systems mit Z |
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| Beschreibung der Erfahrung | |||||||||
| |||||||||
| Die Firma Praxis Critical Systems hat in einem Projekt für Multos eine Certification Authority (CA) modelliert. Die Certification Authority erzeugt die notwendigen Informationen, um die Smart Cards frei zuschalten und Sicherheitszertifikate zu erzeugen, die das Laden und Löschen von Applikationen erlauben. Die CA wurde mit Z spezifiziert. Zur Spezifikation der Prozessstruktur verwendete Praxis CSPs.
Die CA wurde in SPARK, einem Ada-Dialekt, und in ADA 95 umgesetzt. Die grafische Oberfläche wurde mit MFC in C++ umgesetzt. Insgesamt war der Einsatz der formalen Methoden Z, CSP und SPARK erfolgreich. Dafür sprechen die vergleichsweise geringe Fehlerrate von 0.04 Fehlern pro 1000 Zeilen Quelltext und die hohe Durchschnittsproduktivität von 28 Zeilen Code pro Tag pro Entwickler. Details zu diesem Projekt finden sich bei http://www.sparkada.com/ | |||||||||
| |||||||||
| Studienobjekte | |||||||||
| |||||||||
| Smart Cards | |||||||||
| |||||||||
| Studientypen | |||||||||
| |||||||||
| Fallstudie | |||||||||
| |||||||||
| Problemlösung | |||||||||
| |||||||||
| Modellierung einer Certification Authority mit Z und CSP | |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
| |||||||||
Eintrag kommentieren | ||||
| ||||
| ||||
| ||||
| Korrektheit per Konstruktion:... | ||||
| ||||
| ||||
| ||||
| ||||
 | Adressiert Technologien | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| Literaturhinweise | | ||
| ||||
|
| | ||
| ||||
| ||||
| ||||
| Glossar | | ||
| ||||
|
| | ||
|
| | ||
| ||||
| ||||
| | | ||
| ||||||||||||||
|
