面向对象软件规格说明的形式化验证与确认

本课题研究面向对象的形式化软件规格说明的构造、验证和确认的方法与技术，开发相应的支持工具。研究内容包括：研究UML规格说明到Object-Z规格说明的转换；重点研究对Object-Z规格说明进行确认的动画（animation）技术、产生规格说明证明责任（obligation）并对其进行证明的验证方法；探索可应用于软件形式规格说明验证的模型检查方法；开发UML到形式规格说明的转换工具、Object-Z规格说明的动画工具和Object-Z定理证明工具原型。.该课题的研究结合了图形化建模语言UML的可理解性和形式化规格说明语言Object-Z的严密性与精确性的优点，有助于构造面向对象的形式规格说明，并能对所产生的规格说明进行形式化验证和确认。该课题对于提高软件规格说明的可理解性、正确性，提高软件系统，特别是安全关键系统和复杂软件系统的可靠性有十分重要的意义，并可推动形式方法在工业界的应用。