People who live in low-income and hard-to-reach regions are usually the most affected ones by high incidences of arboviral diseases,increasing morbidity and mortality rates,and public health costs.We present the model...People who live in low-income and hard-to-reach regions are usually the most affected ones by high incidences of arboviral diseases,increasing morbidity and mortality rates,and public health costs.We present the modeling of hardware and software components of an unmanned aerial vehicle(UAV)system by mathematical tools,focusing on monitoring foci of arboviral diseases transmitted by Aedes aegypti mosquito,e.g.,Zika,Chikungunya,and Dengue.We used restriction equations and the colored Petri nets formal modeling language to represent the flight dynamics and the software components of the system,respectively.We evaluated the specification of desired behaviors of the monitoring system using simulations and the model checking technique.The results showed the completeness and correctness of the specification.The design of such a system is challenging due to the potential risks to people and the environment.Therefore,this study provides insights into the development of an UAV system for such an application scenario.The monitoring system has the potential of improving the efficiency in identifying foci of arboviral diseases.展开更多
文摘People who live in low-income and hard-to-reach regions are usually the most affected ones by high incidences of arboviral diseases,increasing morbidity and mortality rates,and public health costs.We present the modeling of hardware and software components of an unmanned aerial vehicle(UAV)system by mathematical tools,focusing on monitoring foci of arboviral diseases transmitted by Aedes aegypti mosquito,e.g.,Zika,Chikungunya,and Dengue.We used restriction equations and the colored Petri nets formal modeling language to represent the flight dynamics and the software components of the system,respectively.We evaluated the specification of desired behaviors of the monitoring system using simulations and the model checking technique.The results showed the completeness and correctness of the specification.The design of such a system is challenging due to the potential risks to people and the environment.Therefore,this study provides insights into the development of an UAV system for such an application scenario.The monitoring system has the potential of improving the efficiency in identifying foci of arboviral diseases.