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

Contract-Based Verification of Discrete-Time Multi-Rate Simulink Models

Pontus Boström, Jonatan Wiik, Contract-Based Verification of Discrete-Time Multi-Rate Simulink Models. Software and Systems Modeling , 1–21, 2015.

http://dx.doi.org/10.1007/s10270-015-0477-x

Abstract:

This paper presents an approach to modular contract-based verification of discrete-time multi-rate Simulink models. The verification approach uses a translation of Simulink models to sequential programs that can then be verified using traditional software verification techniques. Automatic generation of the proof obligations needed for verification of correctness with respect to contracts, and automatic proofs are also discussed. Furthermore, the paper provides detailed discussions about the correctness of each step in the verification process. The verification approach is demonstrated on a case study involving control software for prevention of pressure peaks in hydraulics systems.

BibTeX entry:

@ARTICLE{jBoWi15a,
  title = {Contract-Based Verification of Discrete-Time Multi-Rate Simulink Models},
  author = {Boström, Pontus and Wiik, Jonatan},
  journal = {Software and Systems Modeling},
  publisher = {Springer},
  pages = {1–21},
  year = {2015},
  keywords = {Automated verification, Refinement, Control systems, SMT solving, Synchronous data flow},
  ISSN = {1619-1374},
}

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

Publication Forum rating of this publication: level 2

Edit publication