Automatic support for verification of secure transactions in distributed environment using symbolic model checking

被引：0

作者：

Di Sciascio, E ^{[1
]}

Donini, FM ^{[1
]}

Mongiello, M ^{[1
]}

Piscitelli, G ^{[1
]}

机构：

[1] Politecn Bari, Dipartimento Elettrotecn & Elettron, Bari, Italy

来源：

ITI 2001: PROCEEDINGS OF THE 23RD INTERNATIONAL CONFERENCE ON INFORMATION TECHNOLOGY INTERFACES | 2001年

关键词：

e-commerce; model checking; secure transactions;

D O I：

暂无

中图分类号：

TP18 [人工智能理论];

学科分类号：

081104 ; 0812 ; 0835 ; 1405 ;

摘要：

Electronic commerce needs the aid of software tools to check the validity of business processes in order to fully automate the exchange of information through the network. Symbolic model checking has been used to formally verify specifications of secure transactions in a system for business-to-business. The fundamental principles behind symbolic model checking are presented along with techniques used to model mutual exclusion of processes and atomic transactions. The computational resources required to check the example process are presented, and faults detected in this process through symbolic verification are documented.

引用

页码：447 / 454

页数：8

共 50 条

[1] Automatic support for verification of secure transactions in distributed environment using symbolic model checking
Di Sciascio, Eugenio
Donini, Francesco M.
Mongiello, Marina
Piscitelli, Giacomo
[J]. Journal of Computing and Information Technology, 2001, 9 (03) : 185 - 195
[2] A symbolic model checking approach in formal verification of distributed systems
Souri, Alireza
Rahmani, Amir Masoud
Navimipour, Nima Jafari
Rezaei, Reza
[J]. HUMAN-CENTRIC COMPUTING AND INFORMATION SCIENCES, 2019, 9 (01):
[3] Design verification of Web Applications using symbolic model checking
Di Sciascio, E
Donini, FM
Mongiello, M
Totaro, R
Castelluccia, D
[J]. WEB ENGINEERING, PROCEEDINGS, 2005, 3579 : 69 - 74
[4] Formal verification of digital circuits using symbolic model checking
Casar, A
Brezocnik, Z
Kapus, T
[J]. INFORMACIJE MIDEM-JOURNAL OF MICROELECTRONICS ELECTRONIC COMPONENTS AND MATERIALS, 2000, 30 (03): : 153 - 160
[5] Conformance checking of electronic business processes to secure distributed transactions
Talamo, Maurizio
Arcieri, Franco
Schunck, Christian H.
D'Iddio, Andrea Callia
[J]. 2013 47TH INTERNATIONAL CARNAHAN CONFERENCE ON SECURITY TECHNOLOGY (ICCST), 2013,
[6] Automatic verification of fault tolerance using model checking
Yokogawa, T
Tsuchiya, T
Kikuno, T
[J]. 2001 PACIFIC RIM INTERNATIONAL SYMPOSIUM ON DEPENDABLE COMPUTING, PROCEEDINGS, 2001, : 95 - 102
[7] Distributed symbolic model checking for μ-calculus
Grumberg, O
Heyman, T
Schuster, A
[J]. FORMAL METHODS IN SYSTEM DESIGN, 2005, 26 (02) : 197 - 219
[8] Distributed Symbolic Model Checking for μ-Calculus
Orna Grumberg
Tamir Heyman
Assaf Schuster
[J]. Formal Methods in System Design, 2005, 26 : 197 - 219
[9] Distributed symbolic model checking for μ-calculus
Grumberg, O
Heyman, T
Schuster, A
[J]. COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2001, 2102 : 350 - 362
[10] Verification of CTLBDI Properties by Symbolic Model Checking
Chen, Ran
Zhang, Wenhui
[J]. 2019 26TH ASIA-PACIFIC SOFTWARE ENGINEERING CONFERENCE (APSEC), 2019, : 102 - 109

← 1 2 3 4 5 →