摘要
运用形式化方法建模在软件开发过程中可提高目标系统的正确性和可靠性,在此提出了一种利用Z语言进行语义分析的方法。该方法在序列图Z规范的基础上,用属性集表示对象状态,并将序列图的上下文表示为Z形式约束,通过检查上下文约束与对象状态间的一致性对序列图进行语义分析。在此以一个基于学分制的排课系统为例,使用面向对象的形式规格说明语言Z,描述了一个精确、完整的高校排课系统的形式化数学模型。过程显示,该方法具有精确的描述性和很强的抽象性,能为软件系统的开发和验证提供科学的框架。
The modeling with formalized methods can improve the validity and reliability of a target system while develo- ping software. A method to utilize Z language to carry out semantic analysis is proposed. The method indicates the object state by the property set and based on Z specification of the sequence diagram. The context of the sequence diagram is expressed as Z form restraint. The sequence diagram was analyzed semantically by checking the uniformity of context restrant and object state. Taking a class scheduling system based on the credit point system as an example, by using the object-oriented specifica- tion language Z, an accurate and entire mathematics model of the class scheduling system is formally described. The process shows that the method has a precise descriptiveness and high-level abstraction capability, and can provide scientific framework for development and verification of the system.
出处
《现代电子技术》
2012年第12期50-53,共4页
Modern Electronics Technique
关键词
形式化方法
规格说明
Z语言
排课系统
formalized method, specification
Z language
class scheduling system
