The Formal Design Model of a File Management System FMS

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