PROGRAM VERIFICATION TECHNIQUES FOR XML SCHEMA-BASED TECHNOLOGIES

Suad Alagić, Mark Royer, David Briggs

2006

Abstract

Representation and verification techniques for XML Schema types, structures, and applications, in a program verification system PVS are presented. Type derivations by restriction and extension as defined in XML Schema are represented in the PVS type system using predicate subtyping. Availability of parametric polymorphism in PVS makes it possible to represent XML sequences and sets via PVS theories. Powerful PVS logic capabilities are used to express complex constraints of XML Schema and its applications. Transaction verification methodology developed in the paper is grounded on declarative, logic-based specification of the frame constraints and the actual transaction updates. A sample XML application given in the paper includes constraints typical for XML schemas such as keys and referential integrity, and in addition ordering and range constraints. The developed proof strategy is demonstrated by a sample transaction verification with respect to this schema. The overall approach has a model theory based on the view of XML types and structures as theories.

Download


Paper Citation


in Harvard Style

Alagić S., Royer M. and Briggs D. (2006). PROGRAM VERIFICATION TECHNIQUES FOR XML SCHEMA-BASED TECHNOLOGIES . In Proceedings of the First International Conference on Software and Data Technologies - Volume 2: ICSOFT, ISBN 978-972-8865-69-6, pages 86-93. DOI: 10.5220/0001309400860093

in Bibtex Style

@conference{icsoft06,
author={Suad Alagić and Mark Royer and David Briggs},
title={PROGRAM VERIFICATION TECHNIQUES FOR XML SCHEMA-BASED TECHNOLOGIES},
booktitle={Proceedings of the First International Conference on Software and Data Technologies - Volume 2: ICSOFT,},
year={2006},
pages={86-93},
publisher={SciTePress},
organization={INSTICC},
doi={10.5220/0001309400860093},
isbn={978-972-8865-69-6},
}


in EndNote Style

TY - CONF
JO - Proceedings of the First International Conference on Software and Data Technologies - Volume 2: ICSOFT,
TI - PROGRAM VERIFICATION TECHNIQUES FOR XML SCHEMA-BASED TECHNOLOGIES
SN - 978-972-8865-69-6
AU - Alagić S.
AU - Royer M.
AU - Briggs D.
PY - 2006
SP - 86
EP - 93
DO - 10.5220/0001309400860093