Designing Verifiable and Reusable Data Access Layer Using Formal Methods and Design Patterns

摘要

Layering is a concept widely used in computer and software modeling. Many modern information systems are designed and built using a layered model where the function of each layer is specified and well defined. In this paper we will be discussing the layer whose responsibilities include data extraction, manipulation and provision of data to the rest of the application. Common design problems that designers face while designing object oriented system can be resolved by using design patterns. These patterns are reusable solutions used heavily in application framework design. Formal methods are mathematical techniques used to construct models that can be proved for consistency, completeness and correctness of computerized systems. We have applied formal methods to data access layer patterns which has resulted a verifiable recipes for solving data access layer design problems. Our formal models are described using VDM++ specification language and are analyzed and validated using the VDM++ Toolbox.