Formal description of the ADT model of files using RTPA

An abstract data type (ADT) is an abstraction of a data structure that specifies what information can be stored in the ADT and what operations can be done on/by the ADT. The file as a common type plays a primordial role in software system development since it provides a means for manipulating large volumes of information and persistent data. However, the file ADT has not been given a formal semantics. Access to data stored in an ADT is through its interfaces. These interfaces and the operations that they represent should be rigorously defined so as to guarantee that their use will give expected results. This paper illustrates the use of real-time process algebra (RTPA) to formally describe both the data and operations of the file ADT. The difficulties in the file ADT specification are the formal description of its logical and physical models. The logical model of the file ADT is modeled using an indexing mechanism in which each record stored in the file is accessed through its address. The formal model is used in the file management system of RTOS+, a novel real-time operating system developed by the authors. RTPA has been found a very useful notation for describing the behavior of software systems