 |
| | | | | Beschreibung | | Nachdem im Baustein Beispielanwendung Amphion ein konkretes Beispiel betrachtet wurde. Soll in diesem Abschnitt ein Tool vorstellen mit dem es möglich ist, eine Reihe verschiedener Anwendungen zu entwickeln. Es handelt sich um das Tool KeY, welches integriert in Borlands Together 1, die Möglichkeit bietet, JavaCard Anwendungen zu verifizieren. Sowohl Together als auch KeY sind vollständig in Java implementiert und damit Plattform unabhängig. Together ist ein CASE Tool, dass die Modellierung von Software unter Verwendung von UML unterstützt. JavaCard ist eine Teilsprache von Java ohne Threads, Klonen von Objekten, dynamisches Laden von Klassen und Gleitkommaarithmetik. Dadurch kann man Java Anwendungen auf Geräten mit begrenzten Speicher, wie z.B.  Smartcard laufen lassen. KeY ermöglicht im Rahmen eines Entwicklungsprozesses unter Verwendung von UML eine formale Spezifikation und Verifikation der Software. Das System KeY setzt in der Entwurfsphase des Entwicklungsprozesses an und ermöglicht es Klassendiagrammen um formale Spezifikationen anzureichern. Der UML-Standard liefert bereits eine Möglichkeit dies zu tun: OCL (Object Constraint Language). Mit KeY ist es möglich diese Spezifikationen auch in Together einzubringen. Der Benutzer kann Spezifikationen sowohl frei eingeben, als auch Funktionen von KeY nutzen um die Spezifikationen automatisch zu generieren. Dies ist umgesetzt indem die Möglichkeit von Together erweitert wurde, Design Pattern zu instanziieren. Darüber hinaus bietet KeY die Möglichkeit, die Bedingungen formal zu verifizieren, sowohl die reine Spezifikation unabhängig der Implementierung auf Konsistenzeigenschaften zu überprüfen, als auch eine Implementierung daraufhin, ob sie die Bedingungen erfüllt. Hierzu bietet KeY sowohl einen Automatischen Beweiser als auch einen Interaktiven Beweiser.2
Die konzeptionelle Architektur des KeY Systems ist in der folgenden Abbildung zu sehen:
Abbildung 1: Architektur von KeY3
Das CASE Tool wurde um einige Features erweitert, um die entsprechenden Daten an die "`verification middleware"' weiterzugeben und den Benutzter dabei zu unterstützen Formale Spezifikationen durchzuführen. Together bietet bereits von sich aus die Möglichkeit OCL-Spezifikationen in ein UML Modell mit aufzunehmen, jedoch bietet es keinerlei Funktionalität um diese zu verarbeiten. Sie werden wie Kommentare behandelt. Darüber hinaus bietet Together alle Funktionen, die nötig sind um einen Kompletten UML-Entwurf durchzuführen. Die "verification middleware" von KeY stellt die Verbindung zwischen dem CASE Tool und den Beweisern dar. Ihre Aufgabe ist es OCL, Java oder UML in JavaCard Dynamic Logic zu übersetzen, so dass es den Beweisern möglich ist sie zu verifizieren. Es bringt jedoch auch Nachteile mit sich, denn Java ist meist nicht so performant wie . Eine der Hauptideen bei KeY ist es, den Einsatz von formalen Methoden auch solchen Leuten zu ermöglichen, die bislang wenig Erfahrung damit haben. Hierfür wurden Funktionen, wie das instanziieren von Design Patterns um OCL-Spezifikationen erweitert. Außerdem kann der Entwickler selbstständig entscheiden, wie viel formale Spezifikationen er machen möchte. Er kann bereits von wenigen Spezifikationen profitieren. Eine komplette Verifikation ist im allgemeinen allerdings nur mit viel Wissen über formale Methoden möglich.2
Zurück zum Überblick Automatisches Beweisen im Bereich der Softwareentwicklung
Nächster Gliederungspunkt Vergleich von Model Checking mit ATP | |
| | | | | | | | | | | | | Zu dieser Seite wurden noch keine Kommentare oder Bewertungen abgegeben. |
|
| | | | |  | Übergeordnet | | | | | | | | | | | Beispielanwendung KeY | | | | | | Literaturhinweise | | | | | | | | | | | | | |
|
Glossar 
Forschungsprojekte 
Anbieterverzeichnis 
Datenbanksuche 
Highlights 
Eintrag kommentieren
