Deductive Environment for the Analysis of
XML-Specifications
New developments in databases build on
XML [BMP+06]
technologies. Concepts of the relational model can be transferred to XML.
This approach is not unproblematic. Transfer of integrity constraints
causes a problem, some XML-specifications are unsatisfiable.
The project presents tools for the development of XML-specifications. A
formalization of XML-specifications and a transformation for
model checking XML-specifications is developed.
A deductive environment proves an extensive library of theorems with
Isabelle [Pau94].
A transformation generates constraints and
MONA [KMS00]
proves that the constraints are unsatisfiable.
The formalization proves the correctness of the constraints.
Circular XML-specifications are unsatisfiable.
A deductive checker generates F-Logic [KLW95] facts that are checked with
Florid [HLS07]. The project presents a deductive
checker based on circular XML-specifications.
References
| [BMP+06] |
Tim Bray, Eve Maler, Jean Paoli, Michael C. Sperberg-McQueen and François Yergeau.
XML, 2006.
|
| [HLS07] |
Thomas Hornung, Georg Lausen and Florian Schmedding.
Florid, 2007.
|
| [KLW95] |
Michael Kifer, Georg Lausen and James Wu. Logical Foundations of Object-Oriented
and Frame-Based Languages. Journal of the ACM, 42(4):741-843, 1995.
|
| [KMS00] |
Nils Klarlund, Anders Møller and Michael I. Schwartzbach.
MONA Implementation Secrets. LNCS, 2088:182-194,
2000.
|
| [Pau94] |
Lawrence C. Paulson. Isabelle: A Generic Theorem
Prover. LNCS 828. Springer, 1994.
|
