用Z语言描述排课问题的形式化模型  

Describing Formal Model of Class Scheduling Problem with Z Language

作　　者：喻钧[1] 容晓峰[1] 曹子建[1] 

机构地区：[1]西安工业大学计算机科学与工程学院,西安710032

出　　处：《西安工业大学学报》2008年第4期375-382,共8页Journal of Xi’an Technological University

基　　金：西安工业大学校长基金(XAGDXJJ0620)

摘　　要：为了使目标软件系统具有较高的可靠性和正确性、并易于维护,在系统的需求规格说明中引入了形式化方法.使用面向对象的形式规格说明语言Z,以一个复杂的NP完全问题——排课问题为例,描述了构建一个排课系统的形式化模型的过程,并用Java实现了模型中的一个实例.结果表明,形式化模型能够精确地定义和描述目标系统的数据模型、状态和操作,大大提高系统设计和开发的质量.The formal method is introduced into the requirement specification of a target software system, in order that the system has the high reliability and validity, as well as easy maintenance. This paper takes an example -a class scheduling problem for a complex NP-complete problem to study. By using the object-oriented specification language Z, it describes the process of creating a formal model of the class scheduling system. One of the examples in the model is implemented using Java language. As a result, the formal model accurately defines and describes the data model, states and operations of the target system, so it greatly improves the quality of system design and developing.

关 键 词：形式化方法 规格说明语言Z 排课问题 形式化模型 

分 类 号：TP311.52[自动化与计算机技术—计算机软件与理论]