Databases and Information Systems
Sie sind hier: Startseite Research Former Projects DEAXS

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.

Dipl.-Inf. Harald Hiss
Dipl.-Inf. Ahmad El Haj Hussein



[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.