%0 Journal Article
%T 用xyz／e语言描述和验证硬件的行为
%A 韩俊刚？
%A 王岩冰？
%A 沈武威？
%J 软件学报
%P 676-682
%D 1996
%X 本文考虑用时态逻辑语言ｘｙｚ／ｅ描述硬件行为的可行性．作为实例，用ｘｙｚ／ｅ语言描述了一个基于微处理器的容错计算机系统，这种描述可以在ｘｙｚ系统上执行，从而可对系统进行模拟．特别有意义的是利用ｘｙｚ／ｖｅｒｉ验证子系统对所期望的性质进行了形式化证明．本文还将ｘｙｚ／ｅ描述与相应的ｖｈｄｌ（ｖｈｓｉｃｈａｒｄｗａｒｅｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ）描述进行了比较．从中可以看出时态逻辑语言的描述具有其独特的优点.
%K 时态逻辑
%K 硬件描述语言
%K 形式化方法
%U http://www.jos.org.cn/ch/reader/view_abstract.aspx?file_no=19961106&flag=1