基于时态逻辑的微控制器运行时验证系统

摘要

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