由于自动导引车的高效性,精确性和灵活性,自动导引车在制造设施、仓库、配送中心和中转码头等地方得到广泛应用。自动导引车对可靠性要求非常高,形式化方法是保证高可靠性的主要技术,而形式化建模是形式化方法的关键,本文将研究形式化建模方法对自动导引车进行形式化建模,用形式化方法分析证明自动导引车的性质的正确性,本文完成了如下工作。首先,本文简要介绍了形式化方法,主要包含逻辑和形式化验证,在逻辑的介绍中,介绍了命题逻辑,一阶逻辑,时序逻辑和高阶逻辑,形式化验证的介绍中,主要介绍等价性验证,模型检验和定理证明的基本原理及特点。然后深入研究了混杂系统以及混杂系统的建模,混杂系统的形成包含两种方式,一种是在离散模型中添加连续现象,然后添加控制系统,另一种是在连续模型中添加离散现象,然后添加控制系统。接下来本文用混杂自动机对自动导引车进行了建模,为了简化自动导引车系统性质的验证,从自动导引车系统混杂自动机模型中抽象出一个抽象模型,为了保证抽象模型的有效性,本文证明了自动导引车系统混杂自动机原模型与抽象模型之间存在互模拟等价关系。最后,本文用一些关键性质刻画系统的正确性,设计了一些约束保证期望性质的正确性,证明了约束的有效性,分析了约束参数,确定了干扰允许的程度。