随着信息技术的发展,物联网与农业生产相结合产生了“智慧农业”的概念。农业物联网是“智慧农业”的核心技术。在设施农业中,农业物联网充分发挥了智能感知、自动控制的特点,极大的促进了设施农业的智能化建设,有效地改善了农业生产的条件。农业物联网的系统设计是设施农业系统开发生命周期中一个重要阶段,系统设计阶段产生的缺陷会随着系统开发的深入逐渐被放大。形式化方法是一种基于数学的方法对系统设计进行建模与分析的手段。为减少系统设计时产生的错误,本文对农业物联网的特性进行分析,利用形式化方法中的时间自动机理论在系统设计阶段对系统的设计进行建模与模型验证,提供了保证系统设计正确性的方法。本文的主要研究内容与创新有：(1)研究了农业物联网系统结构设计中的模型验证问题,提出了一种基于时间自动机的农业物联网系统结构设计建模与验证的方法。物联网体系结构模型是物联网系统结构设计的参考,当前提出的物联网体系结构模型仅对系统结构进行了描述,并未提供系统设计正确性的验证手段。本文引入时间自动机作为农业物联网系统结构设计建模与模型验证的基础理论,对农业物联网系统结构设计进行分析,根据农业物联网实施的实际情况,将系统结构划分为感执层、网络层与应用层,分别对每层的各个组成部分进行形式化规约,生成感知设备、执行设备、网络、现场控制模块及云端物联网服务的时间自动机模型,最后利用UPPAAL对建立的时间自动机模型进行了形式化验证；(2)研究了农业物联网网关设计的可靠性验证问题,提出了基于时间博弈自动机的农业物联网网关验证方法。针对农业物联网系统中存在控制信号与数据信息并存的信息传输方式,非可控信息的输入会导致系统的运行产生不确定性,非可控信息与可控信号在传输过程中表现为一种博弈状态,本文就此引入了时间博弈自动机对物联网网关信息传输过程进行建模,通过分析物联网系统中的信息传输方式,将信息传输的参与者与物联网网关分别规约为时间博弈自动机模型,对上传的数据信息与下发的控制信号分别进行分析,最后利用模型验证工具UPPAAL-TIGA对物联网网关信息传输过程进行了验证；(3)研究了农业物联网构成的混杂系统形式化建模问题,提出了一种时间自动机的扩展方案。本文以农业物联网系统中的组合服务为研究对象,组合服务由基础服务组合而成,其中既有离散事件子系统又有连续变量子系统,这使系统表现出混杂性。针对系统中的混杂性建模问题,分析了其产生的原因并将系统进行了优化设计,对时间自动机的状态进行分类,把涉及连续变量输入的状态单独进行了划分,指定这类状态的约束关系及状态转换方法,形成时间自动机的扩展方案。最后利用扩展的时间自动机对真实场景下的农业物联网系统进行了形式化建模与验证。