Where academic tradition
meets the exciting future

You are here: TUCS > PUBLICATIONS > Publication Search > An Approach to Contract-Based ...

An Approach to Contract-Based Verification of Simulink Models

Pontus Boström, Richard Grönblom, Tatu Huotari, Jonatan Wiik, An Approach to Contract-Based Verification of Simulink Models. TUCS Technical Reports 985, Turku Centre for Computer Science, 2010.

Abstract:

This paper presents an approach to compositional contract-based verification of Simulink models, together with a tool that supports the approach. First, a format for contracts is presented together with a method to verify models with respect to these contracts. The verification approach uses Synchronous Data Flow (SDF) graphs as an intermediate step to obtain sequential program statements that can then be analysed using traditional refinement-based verification techniques. This gives a convenient approach to calculate the needed proof obligations using well established methods. Secondly, a tool for automatic generation of the proof obligations needed for verification is presented. This tool shows that the approach can be implemented and enables application of the method on practical problems.

Files:

Abstract in PDF-format

Full publication in PDF-format

BibTeX entry:

@TECHREPORT{tBoGrHuWi10a,
  title = {An Approach to Contract-Based Verification of Simulink Models},
  author = {Boström, Pontus and Grönblom, Richard and Huotari, Tatu and Wiik, Jonatan},
  number = {985},
  series = {TUCS Technical Reports},
  publisher = {Turku Centre for Computer Science},
  year = {2010},
  keywords = {Contract-based design, Refinement, Synchronous Data Flow, Formal verification, Automatic verification, SMT solving},
  ISBN = {978-952-12-2473-7},
}

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

Edit publication