随着计算机软硬件系统日益复杂，如何保证其正确性和可靠性成为学术界和工业界共同关注的问题。在诸多的系统分析和验证方法中，模型检测技术是近二十年来最成功的自动验证技术之一。其因自动化程度高，效率高等优点而被广泛应用于有穷状态系统的分析与验证中。 并发进程之间通过传送消息实现协作。但现有的基于进程代数的模型检测工具都不能直接处理进程间的数据传送。本文介绍一个并发传值系统自动验证工具图形用户界面的实现，主要工作如下： ●使用Motif标准图形界面开发工具包实现工具的图形用户界面窗口。 ●给出函数式编程语言SML程序和C语言程序间的一种通信方案。并给出工具自动验证引擎与图形用户界面之间的通信方案以协同完成验证任务。 ●对模型检测反例状态迁移图的图形显示进行讨论，给出了以树状结构图的显示反例状态迁移图的方案 ●扩展工具分析系统的功能，实现系统仿真器。