2015 | OriginalPaper | Buchkapitel
Model-Based Formal Reasoning about Data-Management Applications
verfasst von : Carolina Dania, Manuel Clavel
Erschienen in: Fundamental Approaches to Software Engineering
Verlag: Springer Berlin Heidelberg
Aktivieren Sie unsere intelligente Suche, um passende Fachinhalte oder Patente zu finden.
Wählen Sie Textabschnitte aus um mit Künstlicher Intelligenz passenden Patente zu finden. powered by
Markieren Sie Textabschnitte, um KI-gestützt weitere passende Inhalte zu finden. powered by
Data-management applications are focused around so-called CRUD actions that create, read, update, and delete data from persistent storage. These operations are the building blocks for numerous applications, for example dynamic websites where users create accounts, store and update information, and receive customized views based on their stored data. Typically, the application’s data is required to satisfy some properties, which we may call the application’s data invariants. In this paper, we introduce a tool-supported, model-based methodology for proving that all the actions possibly triggered by a data-management application will indeed preserve the application’s data invariants. Moreover, we report on our experience applying this methodology on a non-trivial case study: namely, an application for managing medical records, for which over eighty data invariants need to be proved to be preserved.