Journal of Software:1999.10(11):1163-1168

The Formal Specification and Property Verification of Interactive User Interface
ZHU Jun,ZHANG Gao,HUA Qing-yi,DAI Guo-zhong
Chart / table
Similar Articles
Article :Browse 2992   Download 2581
Received:July 10, 1998    Revised:September 02, 1998
> 中文摘要: 随着人机交互技术的发展,计算机和用户之间的接口越来越自然,但用户界面管理系统内部的复杂度却大大地增加了.目前提出的新一代用户界面的模型大都停留在概念模型阶段,缺乏对模型的严格描述和证明.该文结合对基于自然交互方式的用户界面的研究成果,归纳出了一个交互式用户界面的通用模型.为了保证系统设计的正确性,文章讨论了如何使用形式化描述语言LOTOS(language of temporal ordering specification)和基于动作的时序逻辑ACTL(action based temporal log
Abstract:With the development of human-computer interactive technology, the interface between computers and users is more and more natural, the management of user interface is becoming more and more complex. Now, the available models of next generation user interface are almost conceptual. The formal specification and property verification to them are necessary. Based on the results of the research on natural interactive user interface, the authors give out a general model of interactive user interface. In order to guarantee the correction of the design of system, it needs to specify and verify it rigidly. The formal description and verification by use of LOTOS (language of temporal ordering specification) and ACTL (action based temporal logic) are given out in this paper. These allow people to study, evaluate and define the dynamic behavior of current user interfaces.
文章编号:     中图分类号:    文献标志码:
基金项目:本文研究得到国家自然科学基金和国家863高科技项目基金资助. 本文研究得到国家自然科学基金和国家863高科技项目基金资助.
Foundation items:
Reference text:


ZHU Jun,ZHANG Gao,HUA Qing-yi,DAI Guo-zhong.The Formal Specification and Property Verification of Interactive User Interface.Journal of Software,1999,10(11):1163-1168