Beweisen statt Testen - H here Zuverl ssigkeit durch die Java Modeling Language

Unser t gliches Leben wird immer st rker von Software durchdrungen; daher ist die Korrektheit von Software von fundamentaler Bedeutung. Gleichzeitig wird Software immer komplizierter; daher sind m chtige Methoden zum Nachweis dieser Korrektheit erforderlich. Der wichtigste Ansatz in dieser Sache – der mathematische Beweis der Korrektheit – gewinnt zusehends an Bedeutung für die industrielle Praxis. Im Folgenden werden die grundlegenden Ideen zu diesem Ansatz erl utert sowie eine aktuelle Sprache, die Java Modeling Language, zusammen mit ihren wichtigsten Werkzeugen zur Realisierung dieses Ansatzes vorgestellt.