An executable object-oriented semantics and its application to firewall verification

被引：0
|
作者：
Kenro Yatake
Takuya Katayama
机构：
[1] Japan Advanced Institute of Science and Technology,
来源：
Software & Systems Modeling | 2011年 / 10卷
关键词：
Object-Oriented; Theorem proving; Simulation; HOL; ML;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
This paper presents a formal executable semantics of object-oriented models. We made it possible to conduct both simulation and theorem proving on the semantics by implementing it within the expressive intersection of the functional programming language ML and the theorem prover HOL. In this paper, we present the definition and implementation of the semantics. We also present a prototype verification tool ObjectLogic which supports simulation and theorem proving on the semantics. As a case study, we show the verification of a practical firewall system.
引用
收藏
页码：515 / 536
页数：21
相关论文
共 50 条
  • [21] Semantics, calculi, and analysis for object-oriented specifications
    Achim D. Brucker
    Burkhart Wolff
    Acta Informatica, 2009, 46 : 255 - 284
  • [22] Algebraic semantics of object-oriented data models
    Zamulin, AV
    TOOLS 24: TECHNOLOGY OF OBJECT-ORIENTED LANGUAGES, PROCEEDINGS, 1998, 24 : 43 - 52
  • [23] Semantics, calculi, and analysis for object-oriented specifications
    Brucker, Achim D.
    Wolff, Burkhart
    ACTA INFORMATICA, 2009, 46 (04) : 255 - 284
  • [24] An object-oriented and executable SysML framework for rapid model development
    Balestrini-Robinson, Santiago
    Freeman, Dane F.
    Browne, Daniel C.
    2015 CONFERENCE ON SYSTEMS ENGINEERING RESEARCH, 2015, 44 : 423 - 432
  • [25] Object-oriented numerical software Trilinos and its application
    An, Weiting
    Cao, Jianwen
    Zhang, Ni
    DCABES 2006 Proceedings, Vols 1 and 2, 2006, : 119 - 123
  • [26] OBJECT-ORIENTED BACKPROPAGATION AND ITS APPLICATION TO STRUCTURAL DESIGN
    HUNG, SL
    ADELI, H
    NEUROCOMPUTING, 1994, 6 (01) : 45 - 55
  • [27] An improved Object-Oriented Modeling Technique and its application
    Wang, LJ
    Chen, XM
    OBJECT-ORIENTED TECHNOLOGY, 1997, : 31 - 34
  • [28] A kind of Object-Oriented Petri Net and its Application
    Liu, Xin
    Yin, Guisheng
    Zhan, Ziying
    ICICSE: 2008 INTERNATIONAL CONFERENCE ON INTERNET COMPUTING IN SCIENCE AND ENGINEERING, PROCEEDINGS, 2008, : 541 - +
  • [29] Object-oriented data model for multiple representation of object semantics
    Toshiba Corp, Ome, Japan
    Syst Comput Jpn, 9 (23-32):
  • [30] An object-oriented data model for multiple representation of object semantics
    Ishimaru, T
    Uemura, S
    SYSTEMS AND COMPUTERS IN JAPAN, 1996, 27 (09) : 23 - 32
12345