Formal verification of Matrix based MATLAB models using interactive theorem proving

• Tipo: Artigo em Revista Científica Internacional
• Data: 2021

Autores

Gauhar, A (Autor) Outra; Rashid, A (Autor) Outra; Hasan, O (Autor) Outra; João Bispo (Autor) FEUP; João M. P. Cardoso (Autor) FEUP

Revista

Título: PeerJ Computer Science

Vol. 7

Página Final: e440

Editora: PEERJ INC

Indexação

ISI Web of Knowledge - 1 Citação

Scopus - 3 Citações

Outras Informações

ID Authenticus: P-00T-QCR

DOI: 10.7717/peerj-cs.440

Abstract (EN): MATLAB is a software based analysis environment that supports a high-level programing language and is widely used to model and analyze systems in various domains of engineering and sciences. Traditionally, the analysis of MATLAB models is done using simulation and debugging/testing frameworks. These methods provide limited coverage due to their inherent incompleteness. Formal verification can overcome these limitations, but developing the formal models of the underlying MATLAB models is a very challenging and time-consuming task, especially in the case of higher-order-logic models. To facilitate this process, we present a library of higher-order-logic functions corresponding to the commonly used matrix functions of MATLAB as well as a translator that allows automatic conversion of MATLAB models to higher-order logic. The formal models can then be formally verified in an interactive theorem prover. For illustrating the usefulness of the proposed library and approach, we present the formal analysis of a Finite Impulse Response (FIR) filter, which is quite commonly used in digital signal processing applications, within the sound core of the HOL Light theorem prover.

Idioma: Inglês

Tipo (Avaliação Docente): Científica

Nº de páginas: 21