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 条
  • [41] A Formal Specification and Verification Framework for Timed Security Protocols
    Li, Li
    Sun, Jun
    Liu, Yang
    Sun, Meng
    Dong, Jin-Song
    [J]. IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2018, 44 (08) : 725 - 746
  • [42] Formal Specification and Verification of Industrial Control Logic Components
    Ljungkrantz, Oscar
    Akesson, Knut
    Fabian, Martin
    Yuan, Chengyin
    [J]. IEEE TRANSACTIONS ON AUTOMATION SCIENCE AND ENGINEERING, 2010, 7 (03) : 538 - 548
  • [43] Formal Specification And Verification Of Reconfigurable Wireless Sensor Networks
    Grichi, Hanen
    Mosbahi, Olfa
    Khalgui, Mohamed
    [J]. 2015 IEEE 12TH INTERNATIONAL MULTI-CONFERENCE ON SYSTEMS, SIGNALS & DEVICES (SSD), 2015,
  • [44] Error-Tolerant Processors: Formal Specification and Verification
    Golnari, Ameneh
    Vizel, Yakir
    Malik, Sharad
    [J]. 2015 IEEE/ACM INTERNATIONAL CONFERENCE ON COMPUTER-AIDED DESIGN (ICCAD), 2015, : 286 - 293
  • [45] Formal specification and verification of the SET/A protocol with an integrated approach
    Lam, VSW
    Padget, J
    [J]. CEC 2004: IEEE INTERNATIONAL CONFERENCE ON E-COMMERCE TECHNOLOGY, PROCEEDINGS, 2004, : 229 - 235
  • [46] Formal Specification, Verification and Repair of Contiki's Scheduler
    Mousavi, Hassan
    Ebnenasir, Ali
    Mahmoudzadeh, Elham
    [J]. ACM TRANSACTIONS ON CYBER-PHYSICAL SYSTEMS, 2023, 7 (04)
  • [47] Using Reo for formal specification and verification of system designs
    Razavi, Niloofar
    Sirjani, Marjan
    [J]. FOURTH ACM & IEEE INTERNATIONAL CONFERENCE ON FORMAL METHODS AND MODELS FOR CO-DESIGN, PROCEEDINGS, 2006, : 113 - +
  • [48] Formal Specification and Verification of Multi-Agent Systems
    Bourahla, Mustapha
    Benmohamed, Mohamed
    [J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 123 : 5 - 17
  • [49] Formal Specification and Verification of a Selective Defense for TDoS Attacks
    Dantas, Yuri Gil
    Lemos, Marcilio O. O.
    Fonseca, Iguatemi E.
    Nigam, Vivek
    [J]. REWRITING LOGIC AND ITS APPLICATIONS, WRLA 2016, 2016, 9942 : 82 - 97
  • [50] UML specification of access control policies and their formal verification
    Koch M.
    Parisi-Presicce F.
    [J]. Software & Systems Modeling, 2006, 5 (4) : 429 - 447
12345