Contract-Based Verification of Simulink Models

被引:0
|
作者
Bostrom, Pontus [1 ]
机构
[1] Abo Akad Univ, Dept Informat Technol, FIN-20520 Turku, Finland
来源
关键词
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 条
  • [41] Contract-based testing for PHP with Praspel
    Dadeau, Frederic
    Giorgetti, Alain
    Bouquet, Fabrice
    Enderlin, Ivan
    JOURNAL OF SYSTEMS AND SOFTWARE, 2018, 136 : 209 - 222
  • [42] Mandatory and Contract-based Shareholding Disclosure
    Enriques, Luca
    Gargantini, Matteo
    Novembre, Valerio
    UNIFORM LAW REVIEW, 2010, 15 (3-4) : 713 - 742
  • [43] On the Significance of Contract-Based Typestate Specification
    Khairunnesa, Samantha Syeda
    Hoan Anh Nguyen
    Rajan, Hridesh
    WASPI'18: PROCEEDINGS OF THE 1ST ACM SIGSOFT INTERNATIONAL WORKSHOP ON AUTOMATED SPECIFICATION INFERENCE, 2018, : 13 - 14
  • [44] Contract-Based Cooperative Spectrum Sharing
    Duan, Lingjie
    Gao, Lin
    Huang, Jianwei
    2011 IEEE INTERNATIONAL SYMPOSIUM ON DYNAMIC SPECTRUM ACCESS NETWORKS (DYSPAN), 2011, : 399 - 407
  • [45] Contract-based mutation for testing components
    Jiang, Y
    Hou, SS
    Shan, JH
    Zhang, L
    Xie, B
    ICSM 2005: PROCEEDINGS OF THE 21ST IEEE INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE, 2005, : 483 - 492
  • [46] ARCHITECTURAL MALPRACTICE - CONTRACT-BASED APPROACH
    不详
    HARVARD LAW REVIEW, 1979, 92 (05) : 1075 - 1102
  • [47] Contract-based testing for web services
    Dai, Guilan
    Bai, Xiaoying
    Wang, Yongbo
    Dai, Fengjun
    COMPSAC 2007: THE THIRTY-FIRST ANNUAL INTERNATIONAL COMPUTER SOFTWARE AND APPLICATIONS CONFERENCE, VOL I, PROCEEDINGS, 2007, : 517 - +
  • [48] Precise and Automated Contract-Based Reasoning for Verification and Certification of Information Flow Properties of Programs with Arrays
    Amtoft, Torben
    Hatcliff, John
    Rodriguez, Edwin
    PROGRAMMING LANGUAGES AND SYSTEMS, PROCEEDINGS, 2010, 6012 : 43 - 63
  • [49] A Contract-Based Formalism for the Specification of Heterogeneous Systems
    Benvenuti, Luca
    Ferrari, Alberto
    Mangeruca, Leonardo
    Mazzi, Emanuele
    Passerone, Roberto
    Sofronis, Christos
    2008 FORUM ON SPECIFICATION, VERIFICATION AND DESIGN LANGUAGES, 2008, : 166 - +
  • [50] Managing Reputation in Contract-Based Distributed Systems
    Baldoni, Roberto
    Doria, Luca
    Lodi, Giorgia
    Querzoni, Leonardo
    ON THE MOVE TO MEANINGFUL INTERNET SYSTEMS: OTM 2009, PT 1, 2009, 5870 : 760 - 772