设施农业物联网系统建模与模型验证

发布时间：2018-06-01 11:44

本文选题：农业物联网 + 设施农业系统　；参考：《中国农业大学》2016年博士论文

【摘要】：随着信息技术的发展,物联网与农业生产相结合产生了“智慧农业”的概念。农业物联网是“智慧农业”的核心技术。在设施农业中,农业物联网充分发挥了智能感知、自动控制的特点,极大的促进了设施农业的智能化建设,有效地改善了农业生产的条件。农业物联网的系统设计是设施农业系统开发生命周期中一个重要阶段,系统设计阶段产生的缺陷会随着系统开发的深入逐渐被放大。形式化方法是一种基于数学的方法对系统设计进行建模与分析的手段。为减少系统设计时产生的错误,本文对农业物联网的特性进行分析,利用形式化方法中的时间自动机理论在系统设计阶段对系统的设计进行建模与模型验证,提供了保证系统设计正确性的方法。本文的主要研究内容与创新有：(1)研究了农业物联网系统结构设计中的模型验证问题,提出了一种基于时间自动机的农业物联网系统结构设计建模与验证的方法。物联网体系结构模型是物联网系统结构设计的参考,当前提出的物联网体系结构模型仅对系统结构进行了描述,并未提供系统设计正确性的验证手段。本文引入时间自动机作为农业物联网系统结构设计建模与模型验证的基础理论,对农业物联网系统结构设计进行分析,根据农业物联网实施的实际情况,将系统结构划分为感执层、网络层与应用层,分别对每层的各个组成部分进行形式化规约,生成感知设备、执行设备、网络、现场控制模块及云端物联网服务的时间自动机模型,最后利用UPPAAL对建立的时间自动机模型进行了形式化验证；(2)研究了农业物联网网关设计的可靠性验证问题,提出了基于时间博弈自动机的农业物联网网关验证方法。针对农业物联网系统中存在控制信号与数据信息并存的信息传输方式,非可控信息的输入会导致系统的运行产生不确定性,非可控信息与可控信号在传输过程中表现为一种博弈状态,本文就此引入了时间博弈自动机对物联网网关信息传输过程进行建模,通过分析物联网系统中的信息传输方式,将信息传输的参与者与物联网网关分别规约为时间博弈自动机模型,对上传的数据信息与下发的控制信号分别进行分析,最后利用模型验证工具UPPAAL-TIGA对物联网网关信息传输过程进行了验证；(3)研究了农业物联网构成的混杂系统形式化建模问题,提出了一种时间自动机的扩展方案。本文以农业物联网系统中的组合服务为研究对象,组合服务由基础服务组合而成,其中既有离散事件子系统又有连续变量子系统,这使系统表现出混杂性。针对系统中的混杂性建模问题,分析了其产生的原因并将系统进行了优化设计,对时间自动机的状态进行分类,把涉及连续变量输入的状态单独进行了划分,指定这类状态的约束关系及状态转换方法,形成时间自动机的扩展方案。最后利用扩展的时间自动机对真实场景下的农业物联网系统进行了形式化建模与验证。
[Abstract]:With the development of information technology, the concept of "intelligent agriculture" is produced by the combination of the Internet of things and agricultural production. The agricultural IOT is the core technology of "intelligent agriculture". In the facilities agriculture, the Internet of things of agriculture has fully developed the intelligent perception and automatic control characteristics, which greatly promoted the intelligent construction of the facilities agriculture and improved effectively. The system design of the Agricultural Internet of things is an important stage in the life cycle of the facility agricultural system development. The defects produced in the system design phase will be gradually enlarged with the deepening of the system development. The formalized method is a means of modeling and analyzing the system design based on the mathematical method. In this paper, the characteristics of the Agricultural Internet of things are analyzed, and the time automaton theory in the formal method is used to model and verify the design of the system in the design stage of the system. The method to ensure the correctness of the system design is provided. The main contents and innovations of this paper are as follows: (1) the research of agricultural products is made. A method of modeling and verification of the structure design of the IOT system based on time automata is proposed. The Internet of things architecture model is a reference for the structure design of the IOT system, and the present IOT architecture model is only described for the system structure, and it has not been proposed. This paper introduces time automata as the basic theory of the structure design modeling and model verification of the Agricultural Internet of things system, analyzes the structure design of the Agricultural Internet of things system. According to the actual situation of the implementation of the Agricultural Internet of things, the structure of the system is divided into the sense level, the network layer and the application layer, respectively. Form the formal specification of each component of each layer, generate the perceptual equipment, implement the equipment, the network, the field control module and the time automaton model of the cloud Internet of things service, and finally make a formal verification of the time automata model established by UPPAAL. (2) the reliability verification problem of the design of the IOT gateway is studied. An agricultural Internet of things gateway verification method based on time game automata is proposed. In the system of Agricultural Internet of things, there is an information transmission mode of coexistence of control signal and data information in the Agricultural Internet of things system. The input of uncontrollable information will lead to the uncertainty of the system operation, and the non controllable information and the controllable signal are shown as a kind of information during the transmission process. In this paper, the time game automaton is introduced to model the information transmission process of the Internet of things gateway. By analyzing the information transmission mode in the IOT system, the participants of the information transmission and the IOT gateway are divided into the time game automaton model respectively, and the data information and the control signals are sent to the next control signal respectively. In the end, the model verification tool UPPAAL-TIGA is used to verify the information transmission process of the IOT gateway. (3) the formal modeling problem of the hybrid system composed of the Agricultural Internet of things is studied, and an extension scheme of the time automata is proposed. This paper is based on the combination service of the IOT system as the research object and the combination service. It is composed of basic service composition, including both discrete event subsystem and continuous variable subsystem, which makes the system confounding. According to the hybrid modeling problem in the system, the causes of the system are analyzed and the system is optimized, the state of the time automata is classified and the state involving the input of the continuous variable is introduced. It is divided separately, specifies the constraint relation of the state and the state transformation method, and forms the extension scheme of the time automata. Finally, the extended time automata is used to form the formal modeling and verification of the agricultural IOT system in the real scene.
【学位授予单位】：中国农业大学
【学位级别】：博士
【学位授予年份】：2016
【分类号】：S126;TP391.44;TN929.5

【相似文献】