Article Preview
Top1. Introduction
A file is an encapsulation of structured data and information in both a logical form and a physical implementation (Hsiao & Harary, 1970; Roberts, 1972; Wang, Ngolah, Tan, et al., 2010). Files can be classified as sequential and random files. The former are files that organize information as a list of ordered records; while the latter are files with sorted records by bi-directional links that can be directly accessed by the key of the record (McDermid, 1991; Wang, Zeng, Ngolah, et al., 2010; Wang, Ngolah, Zeng, et al., 2010). A file can be formally modeled by an abstract data type (Guttag, 1977; Broy et al., 1984; Cardelli & Wegner, 1985; Stubbs & Webre, 1985), which is a logical model of a complex and/or user defined data structure with a set of predefined operations.
A number of ADTs have been identified in computing and system modeling such as stack, queue, sequence, record, array, list, tree, file, and graph (Broy et al., 1984; Wang, 2007; Wang, Ngolah, Tan, et al., 2010). ADTs possess the following properties: (i) An extension of type constructions by integrating both data structures and functional behaviors; (ii) A hybrid data object modeling technique that encapsulates both user defined data structures (types) and allowable operations on them; (iii) The interface and implementation of an ADT are separated. Detailed implementation of the ADT is hidden to applications that invoke the ADT and its predefined operations. Files are a typical ADT in data objects and software modeling, which provides a means for manipulating large volume and persistent information.
A File Management System (FMS) is an indispensable component of operating systems and real-time systems for file manipulation and maintenance. In this paper, the record-level behaviors of files will be modeled by a file ADT; while the system-level behaviors of files will be modeled by the FMS.
In order to rigorously model the file ADT and FMS, the denotational mathematics known as Real-Time Process Algebra (RTPA) (Wang, 2002, 2007, 2008a, 2008b, 2008c, 2008d, 2009a; Wang, Tan, & Ngolah, 2010) is adopted. According to the RTPA methodology for system modeling and refinement, a universal file and the FMS can be formally modeled using two fundamental techniques known as the unified data models and unified process models (Wang, 2007).
Definition 2. A Unified Data Model (UDM) is a generic architectural model of a software system, its internal control structures, and its interfaces with hardware components, which can be rigorously modeled and refined in denotational mathematics as a tuple, i.e.:
(1)Definition 3. The Unified Process Model (UPM) of a program ℘ is a composition of a finite set of m processes according to the time-, event-, and interrupt-based process dispatching rules, i.e.:
(2)