公开(公告)号：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部分中实数型条件值。

公开(公告)号：CN108694285A

公开(公告)日：2018-10-23

申请号：CN201810466424.5

申请日：2018-05-16

Applicant: 南京大学

Inventor： 卜磊 ,  任昕悦 ,  邢少鹏 ,  王佳宛 ,  赵建华 ,  李宣东

IPC: G06F17/50

CPC classification number: G06F17/5009

Abstract: 本发明公开了一种分析组合线性混成自动机全局可达的方法和装置。本发明通过对组合线性混成自动机进行路径编码，编码成相应的SAT约束和SMT约束，经相应的SAT约束求解器和SMT约束求解器求解实现有界模型检验，并在检验过程中利用SMT约束求解器收集不可达路径片段。然后将不可达路径片段编码成相应的LTL约束，通过LTL验证工具验证组合线性混成自动机全局可达性。本发明可验证复杂组合线性混成自动机的全局可达性。