The Formal Design Model of a File Management System (FMS)

The Formal Design Model of a File Management System (FMS)

Yingxu Wang (University of Calgary, Canada), Cyprian F. Ngolah (Sentinel Trending & Diagnostics Ltd., Canada), Xinming Tan (Wuhan University of Technology, China), Yousheng Tian (University of Calgary, Canada) and Phillip C.Y. Sheu (University of California, USA)
Copyright: © 2013 |Pages: 21
DOI: 10.4018/978-1-4666-2651-5.ch014


Files are a typical abstract data type for data objects and software modeling, which provides a standard encapsulation and access interface for manipulating large-volume information and persistent data. File management systems are an indispensable component of operating systems and real-time systems for file manipulations. This paper develops a comprehensive design pattern of files and a File Management System (FMS). A rigorous denotational mathematics, Real-Time Process Algebra (RTPA), is adopted, which allows both architectural and behavioral models of files and FMS to be rigorously designed and implemented in a top-down approach. The conceptual model, architectural model, and the static/dynamic behavioral models of files and FMS are systematically presented. This work has been applied in the design and modeling of a real-time operating system (RTOS+).
Chapter Preview

1. 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.

  • Definition 1: An Abstract Data Type (ADT) is an abstract model of data objects with a formal encapsulation of its logical architecture and predefined operations of the data object.

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.:


  • 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 (Box 1).

Box 1.­

Complete Chapter List

Search this Book: