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 条
  • [1] An executable object-oriented semantics and its application to firewall verification
    Yatake, Kenro
    Katayama, Takuya
    SOFTWARE AND SYSTEMS MODELING, 2011, 10 (04): : 515 - 536
  • [2] An executable semantics of object-oriented models for simulation and theorem proving
    Yatake, Kenro
    Katayama, Takuya
    MSVVEIS 2008: MODELLING, SIMULATION, VERIFICATION AND VALIDATION OF ENTERPRISE INFORMATION SYSTEMS, 2008, : 71 - 80
  • [3] Object-Oriented Operational Semantics
    Prinz, Andreas
    Moller-Pedersen, Birger
    Fischer, Joachim
    SYSTEM ANALYSIS AND MODELING: TECHNOLOGY-SPECIFIC ASPECTS OF MODELS, 2016, 9959 : 132 - 147
  • [4] Object-Oriented MSVL and Its Application
    Wang, Xiaobing
    Duan, Zhenhua
    Tian, Cong
    Zhang, Haibin
    FOURTH INTERNATIONAL CONFERENCE ON MACHINE VISION (ICMV 2011): MACHINE VISION, IMAGE PROCESSING, AND PATTERN ANALYSIS, 2012, 8349
  • [5] On the semantics of object-oriented landmark recognition
    E. Michaelsen
    K. Jäger
    D. Roschkowski
    L. Doktorski
    M. Arens
    Pattern Recognition and Image Analysis, 2012, 22 (1) : 44 - 53
  • [6] Object-oriented action semantics specifications
    Carvilhe, C
    Musicante, MA
    JOURNAL OF UNIVERSAL COMPUTER SCIENCE, 2003, 9 (08) : 910 - 934
  • [7] Verifying Executable Object-Oriented Specifications with Separation Logic
    van Staden, Stephan
    Calcagno, Cristiano
    Meyer, Bertrand
    ECOOP 2010: OBJECT-ORIENTED PROGRAMMING, 2010, 6183 : 151 - +
  • [8] Utilization of extended firewall for object-oriented regression testing
    White, L
    Jaber, K
    Robinson, B
    ICSM 2005: PROCEEDINGS OF THE 21ST IEEE INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE, 2005, : 695 - 698
  • [9] AN EXECUTABLE VISUAL FORMALISM FOR OBJECT-ORIENTED CONCEPTUAL MODELING
    KUNG, DC
    JOURNAL OF SYSTEMS AND SOFTWARE, 1995, 31 (01) : 33 - 43
  • [10] HOOVER: Hardware object-oriented verification
    Aref, MM
    Elleithy, KM
    PROCEEDINGS OF THE 8TH GREAT LAKES SYMPOSIUM ON VLSI, 1998, : 351 - 355
12345