Formal Verification of ABAP by Z Specification

被引:0
|
作者
Rodruksa, Soravit [1 ]
Pradubsuwun, Denduang [1 ]
机构
[1] Thammasat Univ, Fac Sci & Technol, Dept Comp Sci, Bangkok, Thailand
关键词
Formal Verification; ABAP; SAP ERP; Z Specification; Isabelle; HOL;
D O I
暂无
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
This paper has proposed a formal verification of ABAP by Z specification. An ABAP programming language is used to create a customized program in SAP ERP. The program must satisfy a business requirement. It likely has a defect from the developed program. Since a specification is created as the business requirement and a program should have functioned as in the specification, the formal verification is needed to assure the correctness of the function in the program. Both an ABAP program and its specification are translated into Z specification and they are verified by Isabelle in order to ensure that the ABAP program conforms to its specification. We also give some experimental result to show the effectiveness of our method.
引用
收藏
页数:4
相关论文
共 50 条
  • [21] Formal Specification and Verification of Dynamic Parametrized Architectures
    Cimatti, Alessandro
    Stojic, Ivan
    Tonetta, Stefano
    [J]. FORMAL METHODS, 2018, 10951 : 625 - 644
  • [22] FORMAL SPECIFICATION AND VERIFICATION OF ISDN SERVICES IN LOTOS
    YAMANO, K
    JOKANOVIC, D
    ANDO, T
    OHTA, M
    TAKAHASHI, K
    [J]. IEICE TRANSACTIONS ON COMMUNICATIONS, 1992, E75B (08) : 715 - 722
  • [23] Formal Specification and Verification of Mobile Agent Systems
    Kahloul, L.
    Grira, M.
    [J]. INTERNATIONAL JOURNAL OF COMPUTERS COMMUNICATIONS & CONTROL, 2014, 9 (03) : 292 - 304
  • [24] A formal specification for web services composition and verification
    Shi, YL
    Zhang, L
    Liu, B
    Liu, FF
    Lin, LL
    Shi, BL
    [J]. Fifth International Conference on Computer and Information Technology - Proceedings, 2005, : 252 - 256
  • [25] Formal specification and verification of ARM6
    Fox, A
    [J]. THEOREM PROVING IN HIGHER ORDER LOGICS, PROCEEDINGS, 2003, 2758 : 25 - 40
  • [26] Formal Specification and Verification of Transmission Control Protocol
    Jarrar, Abdessamad
    Bellasri, Otman
    Chougdali, Sallami
    Balouki, Youssef
    [J]. ICCWCS'17: PROCEEDINGS OF THE 2ND INTERNATIONAL CONFERENCE ON COMPUTING AND WIRELESS COMMUNICATION SYSTEMS, 2017,
  • [27] VESAR - A PRAGMATIC APPROACH TO FORMAL SPECIFICATION AND VERIFICATION
    ALGAYRES, B
    COELHO, V
    DOLDI, L
    GARAVEL, H
    LEJEUNE, Y
    RODRIGUEZ, C
    [J]. COMPUTER NETWORKS AND ISDN SYSTEMS, 1993, 25 (07): : 779 - 790
  • [28] Formal Specification Technique in Smart Contract Verification
    Lee, Seung-Min
    Park, Soojin
    Park, Young B.
    [J]. 2019 INTERNATIONAL CONFERENCE ON PLATFORM TECHNOLOGY AND SERVICE (PLATCON), 2019, : 7 - 10
  • [29] A survey on formal specification and verification of separation kernels
    Zhao, Yongwang
    Yang, Zhibin
    Ma, Dianfu
    [J]. FRONTIERS OF COMPUTER SCIENCE, 2017, 11 (04) : 585 - 607
  • [30] Specification and Formal Verification of Power Gating in Processors
    Gharehbaghi, Amir Masoud
    Fujita, Masahiro
    [J]. PROCEEDINGS OF THE FIFTEENTH INTERNATIONAL SYMPOSIUM ON QUALITY ELECTRONIC DESIGN (ISQED 2014), 2015, : 604 - +