本发明公开了一种面向可移动物联网应用的形式化验证方法及系统，利用界程演算描述实体的包含关系和行动规则，得到可移动物联网应用运行场景的模型；利用界程逻辑描述运行场景需要满足的性质，得到运行场景性质的界程逻辑公式集合；依次判断可移动物联网应用运行场景的模型是否满足界程逻辑公式集合中的每条界程逻辑公式；若可移动物联网应用运行场景的模型满足界程逻辑公式集合中的所有界程逻辑公式，则不需要对运行场景做出任何调整，否则调整设备的部署位置和/或行动规则，并重新验证。本发明用界程演算精确构建可移动物联网应用运行场景的模型，用界程逻辑严格描述可移动物联网应用运行场景的性质，有效提高了形式化验证的可靠性。