View updatability based on the models of a formal specification

Michael Johnson, Robert Rosebrugh

Research output: Chapter in Book/Report/Conference proceedingConference proceeding contributionpeer-review

19 Citations (Scopus)

Abstract

Information system software productivity can be increased by improving the maintainability and modifiability of the software produced. This latter in turn can be achieved by the provision of comprehensive support for views, since view support allows application programs to continue to operate unchanged when the underlying information system is modified. But, supporting views depends upon a solution to the view update problem, and proposed solutions to date have only had limited, rather than comprehensive, applicability. This paper presents a new treatment of view updates for formally specified information systems. The formal specification technique we use is based on category theory and has been the basis of a number of successful major information system consultancies. We define view updates by a universal property in a subcategory of models of the formal specification, and explain why this indeed gives a comprehensive treatment of view updatability, including a solution to the view update problem. However, a definition of updatability which is based on models causes some inconvenience in applications, so we prove that in a variety of circumstances updatability is guaranteed independently of the current model. The paper is predominantly theoretical, as it develops the theoretical basis of a formal methods technique, but the methods described here are currently being used in a large consultancy for a government Department of Health. Because the application area, information systems, is rarely treated by formal methods, we include some detail about the formal methods used. In fact they are extensions of the usual category theoretic specification techniques, and the solution to the view update problem can be seen as requiring the existence of an initial model for a specification.

Original languageEnglish
Title of host publicationFME 2001: Formal Methods for Increasing Software Productivity - International Symposium of Formal Methods Europe, Proceedings
Place of PublicationHeidelberg, Germany
PublisherSpringer, Springer Nature
Pages534-549
Number of pages16
Volume2021 LNCS
ISBN (Print)3540417915, 9783540417910
Publication statusPublished - 2001
Event10th International Symposium of Formal Methods Europe, FME 2001 - Berlin, Germany
Duration: 12 Mar 200116 Mar 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2021 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349

Other

Other10th International Symposium of Formal Methods Europe, FME 2001
Country/TerritoryGermany
CityBerlin
Period12/03/0116/03/01

Fingerprint

Dive into the research topics of 'View updatability based on the models of a formal specification'. Together they form a unique fingerprint.

Cite this