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 条
  • [31] Object-oriented Case Representation and Its Application in IDS
    Quan, Qian
    Rui, Zhang
    Hong-Yi, Che
    PROCEEDINGS OF THE 8TH IEEE/ACIS INTERNATIONAL CONFERENCE ON COMPUTER AND INFORMATION SCIENCE, 2009, : 301 - 306
  • [32] Object-oriented application frameworks
    Fayad, ME
    Schmidt, DC
    COMMUNICATIONS OF THE ACM, 1997, 40 (10) : 32 - 38
  • [33] Integrating verification and testing of object-oriented software
    Engel, Christian
    Gladisch, Christoph
    Klebanov, Vladimir
    Rummer, Philipp
    TESTS AND PROOFS, 2008, 4966 : 182 - 191
  • [34] MODULAR SPECIFICATION AND VERIFICATION OF OBJECT-ORIENTED PROGRAMS
    LEAVENS, GT
    IEEE SOFTWARE, 1991, 8 (04) : 72 - 80
  • [35] On interoperability verification and testing of object-oriented databases
    Kuo, TY
    Cheung, TY
    DATABASE REENGINEERING AND INTEROPERABILITY, 1996, : 125 - 140
  • [36] An object-oriented framework for the formal verification of processors
    Arditi, L
    Collavizza, H
    ECOOP '95 - OBJECT-ORIENTED PROGRAMMING, 1995, 952 : 215 - 234
  • [37] Verification Technology for Object-Oriented/XML Transactions
    Alagic, Suad
    Royer, Mark
    Briggs, David
    OBJECT DATABASES, 2010, 5936 : 23 - 40
  • [38] Verification of object-oriented programs: A transformational approach
    Apt, Krzysztof R.
    de Boer, Frank S.
    Olderog, Ernst-Ruediger
    de Gouw, Stijn
    JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2012, 78 (03) : 823 - 852
  • [39] Automatic verification of transactions on an object-oriented database
    Spelt, D
    Balsters, H
    DATABASE PROGRAMMING LANGUAGES, 1998, 1369 : 396 - 412
  • [40] THE VERIFICATION, VALIDATION AND TESTING OF OBJECT-ORIENTED SYSTEMS
    GRAHAM, JA
    DRAKEFORD, ACT
    TURNER, CD
    BT TECHNOLOGY JOURNAL, 1993, 11 (03): : 79 - 88
12345