Modern days scientific and commercial applications are fairly large and complex and its reliance on large-scale communication, distributed computing infrastructure and complex software system is growing. Electronic payment systems are at the core of many such financially critical software systems. Any failure in such applications may end up in financial losses and loss of trust of users. It is required that these systems exhibit trustworthy behavior and must be able to tolerate failures or attacks. Trustworthiness is now being addressed as an important issue in development of future software systems. In this paper we outline application of formal methods to ensure trustworthiness of electronic payment systems. B specifications of DigiCash payment system are presented. We have used ProB Model checker and animator for temporal model check and constraint based checking, discover errors due to invariant violation and deadlocks, thereby, validating the specifications. © 2012 Springer-Verlag.
CITATION STYLE
Chandra, G., & Yadav, D. (2012). Analyzing data flow in trustworthy electronic payment systems using event-B. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 6411 LNCS, pp. 325–332). https://doi.org/10.1007/978-3-642-27872-3_48
Mendeley helps you to discover research relevant for your work.