Formal Specification for Spatial Information Databases Integration Framework (SIDIF)
Mustafa Man, Julaily Aida Jusuh, Mohd Shafry Mohd Rahim, Mohammad Zaidi Zakaria
Abstract
This paper discusses the formal validation for spatial information databases integration framework (SIDIF). A SIDIF database is a large, organized body of persistent data, usually associated with computerized software designed to update, query, and retrieve components of the data stored within the system. One of the common difficulties faced by the developer is in designing a robust database system. Even so, in order to solve this matter, developers have to focus their efforts on the formal specifications. The formal specification is supposed to reduce the overall development time. Formal specifications can be used to provide an unambiguous and precise supplement to natural language descriptions. Besides, it can be rigorously validated and verified leading to the early detection of specification errors. Consequently, to validate this problem formally, we specify the SIDIF database framework using Z language and prove by using Z/EVES theorem proven tool. By using this kind of tools, it may help to reduce time, energy and mistake compared to manual theorem proving which can be error task and tedious.
Sommerville I. Software Engineering, 7th ed. UK: Addison-Wesley. 2004.
Mustafa M, Julaily J, Yazid MSM. Bio-Informatics: Formal Specification for DNA Databases System. LAP Lambert Academic Publishing. 2011.
Bowen JP, Hinchey MG. Ten Commandments of Formal Methods. Computer. 1995; 28(4): 56-63.
Babich F, Deotto L. Formal Methods for Specification and Analysis of Communication Protocol. IEEE Communication Surveys & Tutorials. 2002; 4(1): 2-15.
Bowen J. Formal Specification and Documentation Using Z: A Case Study Approach. Thomson Publishing. 2003.
Saaltink M. The Z/EVES System. ZUM, LNCS. 1997.
Mustafa M, Yazid MSM, Khalid S, Aezwani WABW. GIS Spatial Data Visualization Tools for Artificial Reefs Distribution. The 3rd International Conference on Mathematics and Statistics (ICoMS-3). 2008: 25-38.
Mustafa M, Yazid MSM, Aezwani WABW, Zaidi ZM. SPI: Productive Software for Fish Landing Data Collection by Using Wireless Mobile Technology. 1st Regional Conference on Human Resource Development (RESERD2008). Kuala Terengganu. 2008: 45-53.
Parent C, Spaccapietra S. Issues and Approaches of Database Integration. CACM. 1998; 41(5): 166-178.
Parent C, Spaccapietra S, Dupont Y. Model independent assertions for integration of heterogeneous schemas. Very Large Database Journal. 1992; 1: 81-126.
Annual Fisheries 2009. Department of Fisheries, Ministry of Agriculture and Agro-based Industries. http://www.dof.gov.my/641
