Title :
Evolutionary behavior verification to the trustworthy banking software
Author :
Zuo-Wen, Jiang ; Xian-Fei, Tang ; Zhi-Jun, Ding ; Chang-Jun, Jiang
Author_Institution :
Electron. & Inf. Eng. Sch., Tongji Univ., Shanghai, China
Abstract :
Oriented to the goal of high-quality banking softwares, trustworthiness is emerging to be important property. This paper studies how to apply formal methods into the trustworthy property preservation of evolutionary components, focusing on the safety property of the concurrent software behavior, this paper presents a new approach to curb the state explosion problem in the model checking based trustworthiness verification. By adopting the environment reduction paradigm, our method is able to reduce the global states of the system by hiding the internal actions of the environment that does not join in the interleaving composition. The method presented is proved and testified with a bank software case study. Experiment data shows that our method is able to improve the verification efficiency.
Keywords :
banking; distributed processing; evolutionary computation; formal verification; concurrent software behavior; environment reduction paradigm; evolutionary behavior verification; formal method; high-quality trustworthy banking software; interleaving composition; model checking; safety property; state explosion problem; trustworthy property preservation; Banking; Computer networks; Embedded computing; Embedded system; Hardware; Laboratories; Software maintenance; Software testing; Software tools; Systems engineering education; concurrent Software; model checking; state reduction;
Conference_Titel :
Computer Engineering and Technology (ICCET), 2010 2nd International Conference on
Conference_Location :
Chengdu
Print_ISBN :
978-1-4244-6347-3
DOI :
10.1109/ICCET.2010.5486319