Deductive Environment for the Analysis of XML-SpecificationsNew 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.|