邓雪峰,孙瑞志,聂 娟,王文狄,史银雪.基于时间自动机的温室环境监控物联网系统建模[J].农业机械学报,2016,47(7):301-308.
Deng Xuefeng,Sun Ruizhi,Nie Juan,Wang Wendi,Shi Yinxue.Greenhouse Environment Monitoring IOT System Modeling Based on Timed Automata[J].Transactions of the Chinese Society for Agricultural Machinery,2016,47(7):301-308.
摘要点击次数: 967
全文下载次数: 730
基于时间自动机的温室环境监控物联网系统建模   [下载全文]
Greenhouse Environment Monitoring IOT System Modeling Based on Timed Automata   [Download Pdf][in English]
投稿时间:2016-02-05  
DOI:10.6041/j.issn.1000-1298.2016.07.041
中文关键词:  温室  物联网  时间自动机  建模  模型验证
基金项目:“十二五”国家科技支撑计划项目(2015BAK04B01)
作者单位
邓雪峰 中国农业大学 
孙瑞志 中国农业大学 
聂 娟 中国农业大学 
王文狄 中国农业大学 
史银雪 中国农业大学 
中文摘要:由于温室环境的复杂性,系统设计的不合理会直接导致数据的不确定和系统的不稳定。基于体系结构的物联网层次模型对物联网的实施具有指导意义,但是体系结构模型没有提供系统建模工具和模型验证的方法。基于时间自动机理论的建模与模型验证方法是一种对物联网系统建模的有效手段,能在系统设计时提高系统的稳定性,保证系统设计的正确性。通过对智能温室监控物联网系统的分析,从系统实施的角度重新对温室环境监控物联网系统进行了层次划分,利用时间自动机理论对系统中的相应组件进行建模,在对各个子系统分别建模的基础上形成了时间自动机网络模型。最后利用时间自动机建模工具UPPAAL,对已经建立的形式化模型进行了系统逻辑正确性验证与系统执行时序验证。结果表明,利用时间自动机理论及其建模工具UPPAAL可以对智能温室监控物联网系统进行建模及模型验证,可以在系统设计时对系统进行准确的模型分析,避免系统设计错误,降低系统设计缺陷,在系统投入运行中规避设计风险,从而提升系统的稳定性与可靠性,确保系统设计的正确性。
Deng Xuefeng  Sun Ruizhi  Nie Juan  Wang Wendi  Shi Yinxue
China Agricultural University,China Agricultural University,China Agricultural University,China Agricultural University and China Agricultural University
Key Words:greenhouse  internet of things  timed automata  modeling  model verification
Abstract:As an emerging technology, internet of things (IOT) has been widely used in the greenhouse environment monitoring. Because of complexities of greenhouse environment, unreasonable system design can lead to data incorrectness and system un stability. Hierarchical model based on the architecture is instructive to the implementation of IOT. However, the architecture model does not provide a system architecture modeling tool and a model validation method. In comparison, modeling and model validation method based on timed automata theory are effective means for IOT modeling. It could improve the stability of the system and ensure the correctness of the system during system design. Based on the analysis on the intelligent greenhouse monitoring IOT system, from the perspective of system implementation, the hierarchical re division was made based on the greenhouse environment monitoring IOT system. Continuously, the corresponding components of different layers were modeled by using timed automata theory modeling. On the basis of subsystem model, the timed automata network model was formed. Ultimately, the system logic correctness verification and system implementation timing verification were made based on the established formalized model by use of UPPAAL, the timed automata modeling tool. The results show that UPPAAL and timed automata theory can realize modeling and model validation of the intelligent greenhouse IOT system. Moreover, the correct model analysis in system design can avoid design errors, reduce the design defects and avoid risk in system operation. Thus, it can enhance system stability and reliability to ensure the correctness of the system.

Transactions of the Chinese Society for Agriculture Machinery (CSAM), in charged of China Association for Science and Technology (CAST), sponsored by CSAM and Chinese Academy of Agricultural Mechanization Science(CAAMS), started publication in 1957. It is the earliest interdisciplinary journal in Chinese which combines agricultural and engineering. It always closely grasps the development direction of agriculture engineering disciplines and the published papers represent the highest academic level of agriculture engineering in China. Currently, nearly 8,000 papers have been already published. There are around 3,000 papers contributed to the journal each year, but only around 600 of them will be accepted. Transactions of CSAM focuses on a wide range of agricultural machinery, irrigation, electronics, robotics, agro-products engineering, biological energy, agricultural structures and environment and more. Subjects in Transactions of the CSAM have been embodied by many internationally well-known index systems, such as: EI Compendex, CA, CSA, etc.

   下载PDF阅读器