随着数字时代的到来,工程师们研发系统的周期越来越短,对系统的可靠性要求越来越高。图形建模是当今工程领域的一项重要技术。一个系统或是协议在它的分析设计阶段,我们通过建立相应的图形化的模型,使它具有实际系统的某些性质。模型是对系统的抽象,它较易于理解、分析和验证,对模型的验证结果可以直接作用于实际系统,而且纠正错误的成本也相对于实际系统而言比较低。我们构筑一个图形化的建模环境,基于状态机的原理对系统进行图形建模,并定义其应具有的性质。然后分别对系统模型和性质进行形式化,最后通过计算机对其验证。论文利用状态机强大的图形化的描述能力对系统进行描述建模并定义了与之相关的语法以及语义,文中引入了EHA作为中间模型生成系统的LTS,解决了状态机对结构化的破坏问题,最后得出相应的Büchi自动机。研究了如何使用LTL公式表达模型性质并给出LTL公式到Büchi自动机的转换方法。通过对两个自动机的乘积进行判空,可以判断模型是否满足欲验证的性质。由于状态机本身具有并发和层次等特征以及语义的复杂性,所以在模型验证时也面临空间爆炸问题。本文还研究了如何缓解其所带来的空间爆炸问题。