DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述

计算机科学 ›› 2014, Vol. 41 ›› Issue (4): 184-189.

DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述

马莉,钟勇,霍颖瑜

佛山科学技术学院电子与信息工程学院佛山528000;佛山科学技术学院电子与信息工程学院佛山528000;佛山科学技术学院电子与信息工程学院佛山528000

出版日期:2018-11-14 发布日期:2018-11-14
基金资助:
本文受广东省自然科学基金(10152800001000016),佛山市科技发展专项资金(2011AA100061),佛山市产学研专项资金(2012HC10027)资助

DTL-Real-Time Object-Z Specification Language and Implementation on Obligation Authorization Model

MA Li,ZHONG Yong and HUO Ying-yu

Online:2018-11-14 Published:2018-11-14

摘要/Abstract

摘要： Object-Z语言缺乏完整的时态描述能力,如无法表达操作在特定时间之后执行或按某种周期执行等,也不具有操作补偿等概念。针对这些问题,在Object-Z中集成实时概念和分布式时态逻辑,提出DTL-Real-Time Object-Z规格语言,该语言能有效地描述操作的时态驱动、事件驱动、操作补偿等因素,分析和说明了该语言的语法和语义,最后通过对责任授权模型的形式化描述说明了该语言的表达能力和应用。

关键词: 形式化描述语言,责任授权模型,Object-Z,分布式时态逻辑

Abstract: Due to the absence of abilities to describe temporal factors entirely in Object-Z,such as describing the execution of operations at some specific time or in some cycles,and the absence of concept of operation compensation,the paper presented DTL-Real-Time Object-Z:an integration of real-time Object-Z with the Distributed Temporal Logic．The language can express the event-driven,time-driven and compensation factors of operations effectively．The syntax and semantics of the language were analyzed and discussed．Finally,expressiveness and application of the language were showed by formal description of an obligation authorization model．

Key words: Formal description language,Obligation authorization model,Object-Z,Distributed temporal logic

马莉,钟勇,霍颖瑜. DTL-Real-Time Object-Z形式化规格说明语言及其责任授权模型描述[J]. 计算机科学, 2014, 41(4): 184-189. https://doi.org/

MA Li,ZHONG Yong and HUO Ying-yu. DTL-Real-Time Object-Z Specification Language and Implementation on Obligation Authorization Model[J]. Computer Science, 2014, 41(4): 184-189. https://doi.org/

参考文献

[1] 许庆国,缪淮扣,曹晓夏,等．Object-Z规格说明测试用例的自动生成器[J]．软件学报,2011,2(6):1155-1168
[2] 缪淮扣,李刚,朱关铭．软件工程语言—Z[M]．上海:上海科学技术文献出版社,1999
[3] 严吉皞,缪淮扣．基于Object-Z的Web组件形式化建模[J].计算机科学,2012,39(6):383-407
[4] Smith G．An Object-Oriented Approach to Formal Specification[D]．Queensland:Department of Computer Science,University of Queensland,1992
[5] Dong J S,Colton J,Zucconi L．A Formal Object Approach to Real-Time Specification[C]∥Proc of 1996Asia-Pacific Software Engineering Conference．Korea:IEEE,1996
[6] Smith G,Hayes I J．An Introduction to Real-Time Object-Z[J]．Formal Asp．Comput.,2002,13(2):128-141
[7] Brendan M,Dong J S．Blending Object-Z and Timed CSP:An In-troduction to TCOZ[C]∥Proc of International Conference on Software Engineering．Kyoto:IEEE,1998:95-104
[8] 文志诚,李长云,满君丰.用带时钟变量的线性时态逻辑扩充Object-Z[J]．计算机应用研究,2009,26(5):1764-1769
[9] Manuel H,David B,Alexander P．On obligations[C]∥Proc．of 10th European Symposium on Research in Computer Security,LNCS 3679．Heidelberg:Springer-Verlag,2005:98-117
[10] 钟勇,秦小麟,刘凤玉.一种面向DRM的责任授权模型及其实施框架[J].软件学报,2010,21(8):2059-2070
[11] 朱彬,王帅,王娜．使用Object-Z获取形式需求[J]．计算机辅助工程,2008,17(1):87-90
[12] Smith G．The Object-Z specification language[M]．Boston:Kluwer Academic,2000

Metrics

Viewed

Full text

Abstract

Cited

Shared

Discussed