Representation of Raspberry PI Practice in Z Notation

The maker is the pioneer of open source, and the open hardware is the essential tools for the makers. As the typical representative of the open hardware, Raspberry Pi has been widely applied in open source since 2012. Z notation is a formal specification language based on the set theory and the first order predicate logic. So the Z notation can improve the reliability and robustness of the computer system using strict mathematical theory. This paper accomplishes a technical explanation of the concept of open hardware and the organization of the Raspberry pi via utilizing the Z notation. The Z notation of Raspberry pi is more precise and more systematic compared with the other informal specification. This research has great significance for the large-scale popularization of Raspberry pi and open hardware development.