一种智能家居物联网系统验证与修复的方法和装置

摘要

本发明公开了一种智能家居物联网系统验证与修复的方法和装置。本发明通过智能家居设备描述信息和IFTTT规则构建混成自动机模型，然后通过对混成自动机模型的路径分析，找出可能到达系统不安全的路径，然后将这些可达路径编码成SMT约束进行求解，如果存在可达路径对应的SMT约束可解，则根据可解的SMT约束对IFTTT规则This部分中实数型条件值进行修正。修正的方法是通过将可解的SMT约束中的对应的IFTTT规则This部分中实数型条件值参数化后并将整个SMT约束取反，然后消去量词后进行求解，将可解值替换This部分中实数型条件值。

主权项

一种智能家居物联网系统验证与修复的方法，其特征在于，包括以下步骤：S1：获取各种不同产商的智能家居设备描述信息、设定的智能家居设备之间的IFTTT规则以及系统不安全状态；S2：根据所述的智能家居设备描述信息和所述的IFTTT规则构建混成自动机模型；S3：通过SMT约束求解的方法对混成自动机模型进行安全验证，通过判断系统不安全状态是否可达判断系统是否安全；S4：当步骤S3判断出系统为不安全，对所述IFTTT规则This条件中的实数型条件值进行修正，修正后重复步骤S2、S3、S4直到步骤S3判断出系统为安全；其中，所述步骤S3包括以下子步骤：S31：遍历混成自动机的所有路径组，对各个路径组进行可达性分析，找出所有的可达路径组；所述可达性分析为判断路径组在图形结构上是否可能抵达所述的系统不安全状态；所述可达路径组为在图形结构中可能抵达所述的系统不安全状态的路径组；S32：将每个可达路径组编码成对应的SMT约束；S33：将所述SMT约束放入SMT求解器进行求解；假如存在一组可达路径组所对应的SMT约束可解，则判断系统为不安全；所述步骤S4中所述对IFTTT规则This条件中的实数型条件值进行修正包括如下子步骤：S41：将可解的SMT约束中对应的IFTTT规则中This部分实数型条件值参数化，并将整个SMT约束反向编码，得到参数化的并取反的SMT约束；S42：将参数化的并取反的SMT约束量词消去后放入SMT求解器求解，获得各个参数的可解值；S43：用各个参数的可解值替换对应的所述IFTTT规则中This部分实数型条件值。