Contract-Based Verification of Simulink Models

被引：0
|
作者：
Bostrom, Pontus [1 ]
机构：
[1] Abo Akad Univ, Dept Informat Technol, FIN-20520 Turku, Finland
来源：
FORMAL METHODS AND SOFTWARE ENGINEERING | 2011年 / 6991卷
关键词：
REFINEMENT CALCULUS;
D O I：
暂无
中图分类号：
TP31 [计算机软件];
学科分类号：
081202 ; 0835 ;
摘要：
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.
引用
收藏
页码：291 / 306
页数：16
相关论文
共 50 条
  • [1] Contract-based verification of discrete-time multi-rate Simulink models
    Pontus Boström
    Jonatan Wiik
    Software & Systems Modeling, 2016, 15 : 1141 - 1161
  • [2] Contract-based verification of discrete-time multi-rate Simulink models
    Bostrom, Pontus
    Wiik, Jonatan
    SOFTWARE AND SYSTEMS MODELING, 2016, 15 (04): : 1141 - 1161
  • [3] Contract-Based Verification of MATLAB and Simulink Matrix-Manipulating Code
    Wiik, Jonatan
    Bostrom, Pontus
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2014, 2014, 8829 : 396 - 412
  • [4] A Contract-Based Semantics and Refinement for Simulink
    Sun, Quan
    Zhang, Wei
    Wang, Chao
    Liu, Zhiming
    DEPENDABLE SOFTWARE ENGINEERING. THEORIES, TOOLS, AND APPLICATIONS, SETTA, 2022, 13649 : 134 - 148
  • [5] Verification of Contract-based Communicating Systems
    Salauen, Gwen
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (138):
  • [6] Contract-Based Verification of Hierarchical Systems of Components
    Quinton, Sophie
    Graf, Susanne
    SEFM 2008: SIXTH IEEE INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING AND FORMAL METHODS, PROCEEDINGS, 2008, : 377 - 381
  • [7] Towards contract-based verification for autonomous vessels
    Torben, Tobias Rye
    Smogeli, Oyvind
    Glomsrud, Jon Arne
    Utne, Ingrid B.
    Sorensen, Asgeir J.
    OCEAN ENGINEERING, 2023, 270
  • [8] A contract-based semantics and refinement for hybrid Simulink block diagrams
    Sun, Quan
    Zhang, Wei
    Wang, Chao
    Liu, Zhiming
    JOURNAL OF SYSTEMS ARCHITECTURE, 2023, 143
  • [9] Towards Smart Contract-Based Verification of Anonymous Credentials
    Muth, Robert
    Galal, Tarek
    Heiss, Jonathan
    Tschorsch, Florian
    FINANCIAL CRYPTOGRAPHY AND DATA SECURITY. FC 2022 INTERNATIONAL WORKSHOPS, 2023, 13412 : 481 - 498
  • [10] VCC: Contract-based Modular Verification of Concurrent C
    Dahlweid, Markus
    Moskal, Michal
    Santen, Thomas
    Tobies, Stephan
    Schulte, Wolfram
    2009 31ST INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING, COMPANION VOLUME, 2009, : 429 - +
12345