Softwareentwicklung

Integration von CSP-O in die OO-Softwareentwicklung fur die automatische Verifikation ¨

Diplomarbeit

Abteilung Entwicklung korrekter Systeme

vorgelegt von:

Andreea Stamer

Erstgutachter: Prof. Dr. E.-R. Olderog Betreuer: Dipl. Inform. Michael Moller ¨

20. Marz 2006 ¨

 usammenfassung

Der Wunsch, korrekte und zuverl¨ssige Software besonders f¨r sicherheitskritische Aufa u gaben zu entwickeln, kann nur dann Realit¨t werden, wenn der klassische objektoriena tierte (OO) Entwicklungsprozess von Software verbessert wird, indem formale Methoden m¨glichst fr¨h innerhalb des Softwareentwicklungsprozesses eingesetzt werden. Das iel o u ist es, den Entwicklungsprozess von Software-Systemen mathematisch zu fundieren, um Fehler fr¨hzeitig zu finden und diese zu beheben. Das Ergebnis des Einsatzes formau ler Methoden ist nicht nur eine Erh¨hung der Qualit¨t von Software, sondern auch die o a Gew¨hrleistung des korrekten Funktionierens der Systeme. Besonders im Bereich der a sicherheitskritischen Systeme werden solche hohen Anforderungen an die Funktionalit¨t a der Software gestellt, da ein fehlerhaftes Verhalten der verwendeten Software Menschenleben kosten k¨nnte. o In dieser Diplomarbeit wird der an der Carl von Ossietzky Universit¨t Oldenburg a entwickelte Ansatz zur Integration der formalen Spezifikationssprache CSP-O in den OO-Entwicklungsprozess angewandt, um die automatische Analyse und Verifikation im Bereich reaktiver, eingebetteter Software-Systeme einzusetzen und somit die Korrektheit und uverl¨ssigkeit der zu erstellenden Software zu erh¨hen. a o Dieser Ansatz bietet eine Vorgehensweise innerhalb des Designprozesses, die in der vorliegenden Arbeit f¨r die Fallstudie eines Software-Systems E-Mail-Clients“ zum Leu ” sen elektronischer Post durchg¨ngig durchgef¨hrt wird. Dadurch wird die Anwendbarkeit a u dieses Ansatzes demonstriert.

---