UniNet Description of Dining Philosopher Problem  

作　　者：DU Zhuomin HE Yanxiang ZHOU Guofu 

机构地区：[1]School of Computer, Wuhan University, Wuhan 430072, Hubei, China [2]State Key Laboratory of Software Engineering, Wuhan University, Wuhan 430072, Hubei, China

出　　处：《Wuhan University Journal of Natural Sciences》2007年第6期1008-1012,共5页武汉大学学报（自然科学英文版）

基　　金：Supported by the Science and Technology Plan of Hubei Province (2002S4108)

摘　　要：The UniNet specification of Dining Philosopher Problem we presents not only is graphic and intuitionistic but also explicitly indicates the In the specification, static semantics and the the static properties are dynamic semantics. the recorder of the dynamic properties, and the dynamic properties are the track of the static properties change. Accordingly, Dining Philosopher Problem is formally verified by UniNet. Furthermore, the procedure of properties＇ verification is implemented through the graphic-related computing style.The UniNet specification of Dining Philosopher Problem we presents not only is graphic and intuitionistic but also explicitly indicates the In the specification, static semantics and the the static properties are dynamic semantics. the recorder of the dynamic properties, and the dynamic properties are the track of the static properties change. Accordingly, Dining Philosopher Problem is formally verified by UniNet. Furthermore, the procedure of properties＇ verification is implemented through the graphic-related computing style.

关 键 词：static semantics dynamic semantics UNITY Petri net 

分 类 号：TP301.2[自动化与计算机技术—计算机系统结构]