Zusammenfassung
Eine der größten Hürden auf dem Weg zur formalen Verifikation von Software ist die Erstellung und Validierung der hierfür notwendigen formalen Spezifikation. Der Erfolg formaler Methoden bei der industriellen Softwareerstellung hängt also davon ab, ob es zum einen gelingt, die notwendigen Zugangsvoraussetzungen für die Erstellung und Verwendung formaler Objekte gering genug zu machen, und zum anderen davon, formale und informelle Softwaremodelle möglichst eng zu integrieren. Für letzteres bietet die weithin verwendete, objektorientierte Modellierungssprache Unified Modeling Language (UML) einen guten Ansatzpunkt durch ihre semi-formale Untersprache Object Constraint Language (OCL). In der vorliegenden Arbeit zeigen wir, daß es auch für Programmierer ohne formalen Hintergrund prinzipiell möglich ist, formale Teilspezifikationen in OCL zu erstellen. Dies erfolgt durch Auswahl, Instanziierung und Adaption von schematischen OCL-Constraints, die von Spezialisten sorgfältig definiert wurden. Durch die Bindung von OCL-Constraints an Entwurfsmuster wird ein hoher Grad an möglicher Hilfestellung und maschineller Unterstützung erreicht. Durch die Erhebung der Constraints im Rahmen eines konkreten Industrieprojekts wird der Praxisbezug des Ansatzes sichergestellt.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Literatur
Buschmann, F., R. Meunier, H. Rohnert, P. Sommerlad und M. Stal: Pattern-Oriented Software Architecture: A System of Patterns. John Wiley & Sons, New York, 1996.
Dwyer, M. B., G. S. Avrunin und J. C. Corbett: Patterns in Property Specifications for Finite-State Verification. In: Proc. 21st International Conference on Software Engineering, S. 411–420. IEEE Computer Society Press, ACM Press, 1999.
Gamma, E., R. Helm, R. Johnson und J. Vlissides: Design Patterns: Elements of Reusable Object-Oriented Software. Addison-Wesley, Reading/MA, 1995.
Holloway, C. M. und K. J. Hayhurst (Hrsg.): Fourth NASA Langley Formal Methods Workshop, Nr. 3356 in NASA Conference Publication, Hampton, Viginia, 1997.
Knight, J. C, C. L. DeJong, M. S. Gibble und L. G. Nakano: Why Are Formal Methods Not USED More Widely?. In: Holloway, C. M. und Hayhurst [4], S. 1–12.
Meyer, B.: Applying “Design by Contract”. IEEE Computer, 25(10):40–51, Okt. 1992.
Object Modeling Group: Unified Modelling Language Specification, version 1.3, Juni 1999. URL: uml.shl.com:80/docs/UML1.3/99-06-08.pdf.
Rumbaugh, J., I. JACOBSON und G. Booch: The Unified Modeling Language Reference Manual. Object Technology Series. Addison-Wesley, Reading/MA, 1999.
Sattler, T.: Einbindung formaler Constraints in UML Spezifikationen. Interner Bericht 2000-16, Fakultät für Informatik, Universität Karlsruhe, Juni 2000.
Unisys Corp. et al.: XML Metadata Interchange (XMI), Okt. 1998. URL: ftp://ftp.omg.org/pub/docs/ad/98-10-05.pdf/pub/docs/ad/98-10-05.pdf.
Warmer, J. und A. Kleppe: The Object Constraint Language: Precise Modelling with UML. Object Technology Series. Addison-Wesley, Reading/MA, 1999.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2000 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baar, T., Hähnle, R., Sattler, T., Schmitt, P.H. (2000). Entwurfsmustergesteuerte Erzeugung von OCL-Constraints. In: Mehlhorn, K., Snelting, G. (eds) Informatik 2000. Informatik aktuell. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-58322-3_30
Download citation
DOI: https://doi.org/10.1007/978-3-642-58322-3_30
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-67880-9
Online ISBN: 978-3-642-58322-3
eBook Packages: Springer Book Archive