• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Deseo Meeting Scheduler: Towards Automated Verification of Database Integrity Constraints

Ralph-Johan Back, Mikołaj Olszewski, Damian Soriano (Eds.), Deseo Meeting Scheduler: Towards Automated Verification of Database Integrity Constraints, 2008.

Abstract:

Amongst the great diversity and quantity of software being developed nowadays, database applications form a large group of widely used software. They are considered to be of high importance, not only due to the general popularity they already gained, but also to the fact that they are applicable to various, also critical, domains. This in turn brings up the issue of correctness of the developed systems and need for the cautious modelling and verification. In this paper we present a method to formally verify a functionality of database application. We illustrate the technique by modelling in PVS a case study application that has a number of non-trivial behavioural and structural properties. The model we construct forms a theory, in which desired properties of the system can be stated and proven.

Files:

Full publication in PDF-format

BibTeX entry:

@PROCEEDINGS{pBaOlSo08a,
  title = {Deseo Meeting Scheduler: Towards Automated Verification of Database Integrity Constraints},
  editor = {Back, Ralph-Johan and Olszewski, Mikołaj and Soriano, Damian},
  year = {2008},
  keywords = {formal methods, database, verification, modelling, PVS},
}

Belongs to TUCS Research Unit(s): Software Construction Laboratorium

Edit publication