Formalizing Model Inference of MicroPython
Formalizing Model Inference of MicroPython
复制标题
DOI：
10.1109/dsn-w58399.2023.00069
复制
发表时间：
2023-06
期刊：
影响因子：
--
通讯作者：
C. Ferro;Tiago Cogumbreiro;F. Martins
中科院分区：
文献类型：
--
作者：
C. Ferro;Tiago Cogumbreiro;F. Martins
模型检查经常用于验证网络物理系统（CPS）。一个主要的挑战是如何捕获一个代表软件实际行为的模型。模型提取可能会引入错误，可能会影响分析的准确性，包括精度损失，不一致，不一致，过度和欠近似。在本文中，我们形式化并证明了从MicroPython编程语言的一个子集中提取模型的正确性，相对于基于跟踪的语义。提取的模型捕获方法调用的顺序，可以使用Shelley进行模型检查。我们从MicroPython代码的中间表示形式化的提取过程，并证明我们的中间表示的行为是一种正规语言。我们的形式化和理论结果是完全机械化的Coq证明助手。
Model checking has often been used for verifying Cyber-Physical Systems (CPS). A major challenge is how to capture a model that represents the actual behavior of the software. Model extraction can introduce errors that can affect the accuracy of the analysis including loss of precision, inconsistency, non-conformance, and over- and under-approximations.In this paper, we formalize and prove the correctness of extracting a model from a subset of the MicroPython programming language with respect to a trace-based semantics. The extracted models capture the order of method calls and can be model checked using Shelley. We formalize the extraction process from an intermediate representation of MicroPython codes and prove that the behavior of our intermediate representation is a regular language. Our formalization and theoretical results are fully mechanized using the Coq proof assistant.