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
来源：
PROCEEDINGS OF 2017 14TH INTERNATIONAL JOINT CONFERENCE ON COMPUTER SCIENCE AND SOFTWARE ENGINEERING (JCSSE) | 2017年
关键词：
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 条
  • [1] Formal Specification and Verification of CSMA/CD Protocol Using Z
    Shukur, Zarina
    Alias, Nursyahidah
    Idrus, Bahari
    Halip, Mohd Hazali Mohamed
    [J]. JURNAL KEJURUTERAAN, 2009, 21 : 85 - 96
  • [2] Web Service Choreography Verification Using Z Formal Specification
    Rastegari, Y.
    Sajadi, Z.
    Shams, F.
    [J]. INTERNATIONAL JOURNAL OF ENGINEERING, 2016, 29 (11): : 1549 - 1557
  • [3] Formal specification and verification of VHDL
    Bickford, M
    Jamsek, D
    [J]. FORMAL METHODS IN COMPUTER-AIDED DESIGN, 1996, 1166 : 310 - 326
  • [4] Formal Specification and Verification of CRDTs
    Zeller, Peter
    Bieniusa, Annette
    Poetzsch-Heffter, Arnd
    [J]. FORMAL TECHNIQUES FOR DISTRIBUTED OBJECTS, COMPONENTS, AND SYSTEMS, 2014, 8461 : 33 - 48
  • [5] FORMAL FOUNDATION FOR SPECIFICATION AND VERIFICATION
    LAMPORT, L
    SCHNEIDER, FB
    [J]. LECTURE NOTES IN COMPUTER SCIENCE, 1985, 190 : 203 - 285
  • [6] Heterogeneous formal specification based on Object-Z and statecharts: semantics and verification
    Gruer, JP
    Hilaire, V
    Koukam, A
    Rovarini, P
    [J]. JOURNAL OF SYSTEMS AND SOFTWARE, 2004, 70 (1-2) : 95 - 105
  • [7] FORMAL SPECIFICATION AND VERIFICATION OF MICROPROCESSOR SYSTEMS
    JOYCE, JJ
    [J]. MICROPROCESSING AND MICROPROGRAMMING, 1988, 24 (1-5): : 371 - 378
  • [8] Formal specification and verification of hardware designs
    Ramesh, S
    Rao, SSSP
    Sivakumar, G
    Bhaduri, P
    [J]. PHOTOMASK AND X-RAY MASK TECHNOLOGY V, 1998, 3412 : 261 - 268
  • [9] FORMAL TECHNIQUES FOR SYSTEMS SPECIFICATION AND VERIFICATION
    CARMO, J
    SERNADAS, A
    [J]. INFORMATION SYSTEMS, 1991, 16 (03) : 245 - 272
  • [10] Formal specification and verification of a micropayment protocol
    Gouda, MG
    Liu, AX
    [J]. ICCCN 2004: 13TH INTERNATIONAL CONFERENCE ON COMPUTER COMMUNICATIONS AND NETWORKS, PROCEEDINGS, 2004, : 489 - 494
12345