TY - GEN
T1 - Formalizing Model Inference of MicroPython
AU - De Ferro, Carlos Mao
AU - Cogumbreiro, Tiago
AU - Martins, Francisco
N1 - Publisher Copyright:
© 2023 IEEE.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
KW - formalization
KW - micropython
KW - model-checking
KW - model-extraction
UR - https://www.scopus.com/pages/publications/85169432920
UR - https://www.scopus.com/pages/publications/85169432920#tab=citedBy
U2 - 10.1109/DSN-W58399.2023.00069
DO - 10.1109/DSN-W58399.2023.00069
M3 - Conference contribution
AN - SCOPUS:85169432920
T3 - Proceedings - 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops Volume, DSN-W 2023
SP - 283
EP - 289
BT - Proceedings - 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops Volume, DSN-W 2023
PB - Institute of Electrical and Electronics Engineers Inc.
T2 - 53rd Annual IEEE/IFIP International Conference on Dependable Systems and Networks Workshops Volume, DSN-W 2023
Y2 - 27 June 2023 through 30 June 2023
ER -