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

Contract-Based Verification of Simulink Models

Pontus Boström, Contract-Based Verification of Simulink Models. In: Shengchao Qin, Zongyan Qiu (Eds.), 13th International Conference on Formal Engineering Methods, ICFEM 2011, Lecture Notes in Computer Science 6991, 291–306, Springer, 2011.

http://dx.doi.org/10.1007/978-3-642-24559-6

Abstract:

This paper presents an approach to compositional contract-based verification of Simulink models. The verification approach uses Synchronous Data Flow (SDF) graphs as a formalism to obtain sequential program statements that can then be analysed using traditional refinement-based verification techniques. Automatic generation of the proof obligations needed for verification of correctness with respect to contracts, as well as automatic proofs are also discussed.

BibTeX entry:

@INPROCEEDINGS{inpBostrom_Pontus11a,
  title = {Contract-Based Verification of Simulink Models},
  booktitle = {13th International Conference on Formal Engineering Methods, ICFEM 2011},
  author = {Boström, Pontus},
  volume = {6991},
  series = {Lecture Notes in Computer Science},
  editor = {Qin, Shengchao and Qiu, Zongyan},
  publisher = {Springer},
  pages = {291–306},
  year = {2011},
  keywords = {Formal verification, SMT-solving, Control systems, Refinement},
}

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

Publication Forum rating of this publication: level 1

Edit publication