Using Formal Methods to Design a Class Scheduling System

Formal methods are introduced into system design process that use rigorously specified mathematical models to build target systems. It can establish a precise and unambiguous model of a complex system. This paper takes an example for a complex NP-complete problem such as a class scheduling problem. By using the specification language Z, it designs and describes a formal mathematical model of a class scheduling system. This formal model is actually Z specifications of the systempsilas data model, system state and operations. The specification can effectively improve system reliability, design time and comprehensibility. Therefore it greatly improves the quality of system design and developing.