基于时态逻辑的微控制器运行时验证方法

摘要

本发明公开了一种基于时态逻辑的微控制器运行时验证方法，包括事件接收步骤，事件预处理步骤，用户编辑步骤、LTL验证步骤。其中，事件接收步骤接收微控制器发出的事件序列；事件预处理步骤对事件接收步骤接收到的事件预处理，将事件转换成一个个独立的原子命题，建立起变量标识与原子命题之间的一一映射，并且输出事件序列字符串；用户编辑步骤给用户提供编辑界面，以供用户编辑原子命题以及LTL公式；LTL验证步骤验证微控制器执行事件序列字符串是否满足用户输入的LTL公式。本发明可以实现微控制器的实时验证，获得微控制器的可能性输出空间，人工鉴别出一些非法事件。