Models & Optimisation and Mathematical Analysis Journal
Volume 1, Numéro 2, Pages 14-20
2012-12-17
Formal Specification By Coq Of Date And Darwen’s Object/relational Model
Authors : Benabbou El . Nait Bahloul Safia .
Abstract
Development of databases software systems would be provided with a high-level specification, suitable for formal reasoning about application-level security and correctness properties. Formal specification is a key element of formal methods. It can greatly increase comprehension of a system by revealing inconsistencies, ambiguities, and incompleteness that might occur. Thus, implementation would be proven correct with respect to this specification to ensure that a bug cannot lead to non-conformance of properties or accidental corruption. It is for these reasons that we see verified DBMSs as a compelling challenge to the development of software. As a step toward this goal, we establish in this paper formalization through a formal specification of some basis concepts in object/relational model proposed by Date and Darwen, using the Coq proof assistant system. We give the challenges acquired from our experience using that proof tool. Our work is a preamble step toward a fully-verified object/relational DBMS.
Keywords
Formal specification, proof assistant system, Coq, verification, object/relational model.
Les articles similaires
Nia Billal
.
Mehenni Mokhtar
.
Rekis Abdelkrim
.
Roumani Messaoud
.
Ben Salah Mohamed Kamel
.
Ben Sayeh Faiza
.
Benouamane Ourida
.
pages 7-11.
خديجة باللودمو
.
ص 08-18.
قيط ليندة
.
بلحنيش عبد الرحمن
.
ص 49-65.
Zerguini L.
.
Martineau P.
.
pages 79-87.
