用xyz／e语言描述和验证硬件的行为

本文考虑用时态逻辑语言ｘｙｚ／ｅ描述硬件行为的可行性．作为实例，用ｘｙｚ／ｅ语言描述了一个基于微处理器的容错计算机系统，这种描述可以在ｘｙｚ系统上执行，从而可对系统进行模拟．特别有意义的是利用ｘｙｚ／ｖｅｒｉ验证子系统对所期望的性质进行了形式化证明．本文还将ｘｙｚ／ｅ描述与相应的ｖｈｄｌ（ｖｈｓｉｃｈａｒｄｗａｒｅｄｅｓｃｒｉｐｔｉｏｎｌａｎｇｕａｇｅ）描述进行了比较．从中可以看出时态逻辑语言的描述具有其独特的优点.