交互式用户界面的形式化描述与性质验证

• 作者: 华庆一 张高 戴国忠 朱军
• 来源期刊: 软件学报
• 学科: 工学
• 关键词: 交互式用户界面 形式化方法 模型检查 时序逻辑 LOTOS ACTL
• 年，卷（期）: 1999,（11）
• 页码范围: 1163-1168
• 页数: 6页
• 分类号: TP311
• 字数: 4466字
• 语种: 中文

摘要

随着人机交互技术的发展,计算机和用户之间的接口越来越自然,但用户界面管理系统内部的复杂度却大大地增加了.目前提出的新一代用户界面的模型大都停留在概念模型阶段,缺乏对模型的严格描述和证明.该文结合对基于自然交互方式的用户界面的研究成果,归纳出了一个交互式用户界面的通用模型.为了保证系统设计的正确性,文章讨论了如何使用形式化描述语言LOTOS(language of temporal ordering specification)和基于动作的时序逻辑ACTL(action based temporal logical)对系统进行描述与验证,这有利于人们对交互式用户界面的动态行为进行研究、评估与定义.

作者信息

序号	姓名	单位	发文数	被引次数	H指数	G指数
1	朱军	中国科学院软件研究所计算机科学开放研究实验室	40	288	9.0	15.0
2	华庆一	西北大学计算机科学系	59	438	10.0	19.0
3	张高	中国科学院软件研究所计算机科学开放研究实验室	1	46	1.0	1.0
4	戴国忠	西北大学计算机科学系	1	46	1.0	1.0