高可靠性温室环境测控系统架构形式化建模与特性证明  

Reliable Greenhouse Environment Monitor and Control System Architecture:Modeling and Reasoning

作　　者：袁凌[1] 李国徽[1] 张晓芳[1] 

机构地区：[1]华中科技大学计算机科学学院,武汉430074

出　　处：《小型微型计算机系统》2012年第8期1723-1729,共7页Journal of Chinese Computer Systems

基　　金：国家教育部博士点基金项目(20090142120025)资助;教育部留学回国人员科研启动基金项目(教外司留[2010]1174)资助

摘　　要：温室环境测控系统由多个可并发执行的子系统共同协作来构造适宜的温室环境以确保作物有效生长.为提高温室环境测控系统设计的效率和可靠性,本文提出一个能为设计者提供指导性框架的融入容错技术的高可靠性温室环境测控系统架构.并且运用PVS形式化语言对系统架构进行了精确而无二义性的形式化建模,以及PVS证明工具对系统架构的容错特性进行了机械化证明,以确保系统架构能满足高可靠性需求.The greenhouse environment monitor and control system is composed of several concurrently interacting subsystems.In order to guarantee the efficient growth of crops in the greenhouse environment,we propose a reliable greenhouse environment monitor and control system architecture.The proposed architecture can provide a generic framework to guide the development of the greenhouse environment system.The PVS language is used to formally model the proposed architecture accurately.Furthermore,in order to verify that the proposed architecture can satisfy high reliability requirements,the PVS theorem prover is used to reason about the fault tolerant properties of the proposed architecture mechanically.

关 键 词：系统架构 PVS系统 容错 形式化建模 形式化证明 

分 类 号：TP311[自动化与计算机技术—计算机软件与理论]