公开(公告)号：CN106055318A

公开(公告)日：2016-10-26

申请号：CN201610343482.X

申请日：2016-05-23

Applicant: 南京大学

Inventor： 卜磊 ,  熊文 ,  任昕悦 ,  王熙 ,  马娆 ,  沈思远 ,  王亚楠 ,  李宣东

IPC: G06F9/44 ,  G06F9/45

CPC classification number: G06F8/34 ,  G06F8/41

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

公开(公告)号：CN106055318B

公开(公告)日：2019-04-12

申请号：CN201610343482.X

申请日：2016-05-23

Applicant: 南京大学

Inventor： 卜磊 ,  熊文 ,  任昕悦 ,  王熙 ,  马娆 ,  沈思远 ,  王亚楠 ,  李宣东

IPC: G06F8/34 ,  G06F8/41

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