Formal description of the ADT model of B-Trees

Formal specification of abstract data types (ADTs) is important in modeling system architecture and their implementations. B-Trees are one of the most widely used ADT in system development. This paper presents a formal approach to the specification of B-Tree using real-time process algebra (RTPA), which is a newly developed mathematics-based notation system for the specification and refinement of real-time and safety-critical systems. The logical model of B-Tree has been abstracted first. The RTPA specification of B-Tree is based on the logical model. In the RTPA specification, B-Tree has been formally described in three parts: system architecture, static behaviors, and dynamic behaviors. In the architectural specification, both logical model and physical implementation model of B-Tree has been specified. The logical model of B-Tree uses RTPA component logical models to present the structure of a B-Tree by nodes and characteristics; while the physical implementation model of B-Tree uses linked list to describe the implementation of a B-Tree. In the behavioral specification, three kinds of B-Tree behaviors, namely traversal operations, manipulation operations, and query operations, have been abstracted and specified by RTPA processes. This work is a part of the effort to build an ADT library for RTPA in the RTPA-based code generation project