• TUCS Publication Series
• How to Publish in TUCS Series
• Publication Search
• Publication Graph
• Publication Input
• Publication Input Guide
• JuFo Browser

Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code

Jonatan Wiik, Pontus Boström, Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code. TUCS Technical Reports 1107, TUCS, 2014.

Abstract:

MATLAB/Simulink is a popular toolset for developing embedded software. The main target of the MATLAB/Simulink toolset is numerical computing applications and the tools offer a rich language for manipulating matrices. This paper presents an approach to automatic, modular, contract-based verification of programs written in a subset of the MATLAB programming language, with focus on efficiently handling the provided matrix manipulation functions. We restrict ourselves to the subset of MATLAB suitable for code generation, which means matrix types and shapes can be determined statically. We present an approach to type and shape inference for matrices that is more strict than MATLAB, but aids verification. The type and shape information is then used in the verification. From the programs and contracts we generate verification conditions that are discharged with an of-the-shelf SMT solver. We present two approaches for verification: direct axiomatisation of built-in matrix functions and expansion of the functions. We evaluate our approaches on a number of examples and discuss challenges for automatic verification in this setting. We found that expansion of matrix functions can be very effective when the matrix sizes are relatively small, which is common in many embedded applications.

Files:

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tWiBo14a,
  title = {Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code},
  author = {Wiik, Jonatan and Boström, Pontus},
  number = {1107},
  series = {TUCS Technical Reports},
  publisher = {TUCS},
  year = {2014},
}

Belongs to TUCS Research Unit(s): Distributed Systems Laboratory (DS Lab)

Edit publication