Modeling and formal verification of smart environments
Periodicals(2014)
摘要
AbstractSmart environments SmE are a growing combination of various computing frameworks ubiquitous, pervasive etc., devices, control algorithms, and a complex web of interactions. It is at the core of user facilitation in a number of industrial, domestic, and public areas. On the basis of their application areas, SmE may be critical in terms of correctness, reliability, safety, security, etc. To achieve error-free and requirement-compliant implementation, these systems are designed by resorting to various modeling approaches including ontology and statecharts. This paper attempts to consider correctness, reliability, safety, and security in the design process of SmE and their related components by proposing a design time modeling and formal verification methodology. The proposed methodology covers various design features related to modeling and formal verification of SmE focusing on users, devices, environment, control algorithms, and their interaction against the set of the requirements through model checking. A realistic case study of a Bank Door Security Booth System BDSB is tested. The results show the successful verification of the properties related to the safety, security, and desired reliable behavior of BDSB. Copyright © 2013 John Wiley & Sons, Ltd.
更多查看译文
关键词
user behavior,smart environments,intelligent domotic environment,modeling,formal verification,model checking,temporal logic
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络