Formal Specifications and Analysis of Requirements in Software Development

Georg Droschl

    Publikation: AbschlussarbeitDissertation

    Abstract

    Diese Dissertation vergleicht zwei Software Entwicklungsmethoden im Rahmen einer Fallstudie. Ein etablierter Ansatz wird der `light-weight Vienna Development Method` gegenübergestellt, welche auf den mathematischen Grundlagen von Mengenlehre und Prädikatenlogik aufbaut. In einer Folge von Entwicklungsschritten werden zunehmend genauere formale Beschreibungen der Software entwickelt. Durch die Anwendung von Testfällen kann überprüft werden, ob eine Beschreibung die Eigenschaften der vorhergehenden Beschreibung erfüllt. Zum Zweck des Vergleichs wurde ein Teil eines bestehenden Sicherheitssystems ausgewählt, dessen gewünschte Funktionalität durch ein `User Requirements Document` definiert ist. Nach-dem das Nachwächterrunden Modul` mit der `light-weight Vienna Development Method` neu entwickelt war, konnten die zwei Implementierungen verglichen werden. Das wichtigste Ergebnis der vorliegenden Dissertation ist, dass die `light-weight Vienna Development Method` die Softwarequalität wesentlich verbessert hat, während der Entwicklungsaufwand etwa gleichgeblieben ist. Weiters wird durch formale Beweise in dem `Prototype Veriflcati-on System` gezeigt, dass das gegebene `User Requirements Document` ungewollte Eigenschaf-ten hat. Schliesslich wird ein Vorschlag gemacht, wie die `light-weight Vienna Development Me-thod` weiter verbessert werden könnte, indem ein neuer Ansatz zur Formalisierung von Requi-rements vorgeschlagen wird. This thesis compares two software development methods within the context of a oase study. A well-established approach is contrasted with the light-weight Vienna Development Method, which is based on the mathematical concepts of set theory and predicate calculus. In a series of development steps, a piece of software is described by increasingly detailed documents. Through the application of test cases, it can be checked whether a description satisfies the properties of the preceding one. For the purpose of the comparison, one module of an existing security system was selected. The desired functionality of the Guardrounds Module had been specified in a User Requirements Document. After re-development using the light-weight Vienna Development Method, the two implementations were compared. The principal result of this thesis is that the light-weight Vienna Development Method has significantly increased software quality while the development effort was comparable. Furthermore, the given User Requirements Document is shown to contain undesirable properties by conducting formal proof in the Prototype Verification System. Finally, a suggestion is made as to how the Iight-weight Vienna Development Method could be improved by a new approach to the formalization of requirements.
    OriginalspracheEnglisch
    Gradverleihende Hochschule
    • Graz University of Technology
    PublikationsstatusVeröffentlicht - 2000

    Research Field

    • Nicht definiert

    Fingerprint

    Untersuchen Sie die Forschungsthemen von „Formal Specifications and Analysis of Requirements in Software Development“. Zusammen bilden sie einen einzigartigen Fingerprint.

    Diese Publikation zitieren