Formal Verification of Ad Hoc M-Commerce Trading Systems with SPIN
Article No.: 78, Pages 1 - 6
Abstract
Ad hoc m-commerce is an emerging application area for ad hoc wireless networks. It provides an alternative way for users to carry out m-commerce transactions without relying on any infrastructure support from a network service provider. Thus, the reliability of ad hoc m-commerce trading systems is important to increase users' confidence in the safety and correctness of the trading system. However, due to the nature of an ad hoc wireless network such as its lack of network infrastructures, having a dynamic network topology and so on, designing a reliable ad hoc m-commerce trading system is a challenging task. Such trading systems with complex processes may not function in an expected way or may be prone to failure due to common design flaws such as system deadlock. This paper presents a formal verification of ad hoc m-commerce trading system processes using the SPIN model checker that aims to verify certain safety properties. The verification results verify that the ad hoc m-commerce trading system is free from system deadlock and satisfies the specified safety properties.
References
[1]
SPIN Website, {cited 30/04/16}. Available from: http://spinroot.com.
[2]
BPMN website, {cited 30/04/16}. available from: http://www.bpmn.org.
[3]
N. Akhtar and M. Nauman. Timed-Automata Based Model-Checking of a Multi-Agent System: A Case Study. Journal of Software Engineering and Applications, 8:43--50, 2015. Scientific Research Publishing.
[4]
A. Amirat, A. Menasria, M. A. Oubelli, and N. Younsi. Automatic Generation of PROMELA Code from Sequence Diagram with Imbricate Combined Fragments. In Second International Conference on Innovative Computing Technology (INTECH), pages 111--118. IEEE, 2012.
[5]
G. J. Holzmann. The model checker spin. IEEE Transactions on Software Engineering, 23(5):279--295, 1997. ACM Digital Library.
[6]
H. Osman and H. Taylor. Managing Group Membership in Ad Hoc M-commerce Trading Systems. In Proceedings of 10th. Annual International Conference on New Technologies of Distributed Systems, pages 173--180. IEEE, 2010.
[7]
H. Osman and H. Taylor. Identity Support in a Security and Trust Service for Ad Hoc M-commerce Trading Systems. In Proceedings of 2011 IEEE Workshops of International Conference on Advanced Information Networking and Applications (WAINA), pages 285--290. IEEE, 2011.
[8]
H. Shi, W. Ma, M. Yang, and X. Zhang. A Case Study of Model Checking Retail Banking System with SPIN. Journal of Computer, 7(10), 2012. Academy Publisher.
[9]
H. Osman, M. Abdullah and N. Ahmad. A Fully Distributed Reputation System for M-commerce via Ad Hoc Wireless Networking. International Journal of Advanced and Applied Sciences (IJAAS), Vol(4), Issue(3), pages 31--40, IASE, 2017.
[10]
H. Osman and H. Taylor. Towards a Reference Model for M-commerce over Ad Hoc Wireless Networks. In Proceedings of E-Activity & Leading Technologies Conference, IASK, pp. 223--232.
Index Terms
- Formal Verification of Ad Hoc M-Commerce Trading Systems with SPIN
Recommendations
Ad hoc routing protocol verification through broadcast abstraction
FORTE'05: Proceedings of the 25th IFIP WG 6.1 international conference on Formal Techniques for Networked and Distributed SystemsWe present an improved method for analyzing route establishment in ad hoc routing protocols. An efficient abstraction for Propagating Localized Broadcast with Dampening (PLBD) is developed. Applying this result we are able to verify networks and ...
Formal verification of ASMs using MDGs
We present a framework for the formal verification of abstract state machine (ASM) designs using the multiway decision graphs (MDG) tool. ASM is a state based language for describing transition systems. MDG provides symbolic representation of transition ...
Formal verification of secure ad hoc routing protocols using AVISPA: ARAN case study
ECC'10: Proceedings of the 4th conference on European computing conferenceFormal verification through model checking proved to be a very useful validation technique for security protocols: authentication, key agreement, non-repudiation, confidentiality, etc. But it has not been yet fully applied for the security properties of ...
Comments
Please enable JavaScript to view thecomments powered by Disqus.Information & Contributors
Information
Published In
January 2018
628 pages
ISBN:9781450363853
DOI:10.1145/3164541
Copyright © 2018 ACM.
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]
In-Cooperation
- SKKU: SUNGKYUNKWAN UNIVERSITY
Publisher
Association for Computing Machinery
New York, NY, United States
Publication History
Published: 05 January 2018
Check for updates
Author Tags
Qualifiers
- Short-paper
- Research
- Refereed limited
Conference
IMCOM '18
IMCOM '18: The 12th International Conference on Ubiquitous Information Management and Communication
January 5 - 7, 2018
Langkawi, Malaysia
Acceptance Rates
IMCOM '18 Paper Acceptance Rate 100 of 255 submissions, 39%;
Overall Acceptance Rate 213 of 621 submissions, 34%
Contributors
Other Metrics
Bibliometrics & Citations
Bibliometrics
Article Metrics
- 0Total Citations
- 34Total Downloads
- Downloads (Last 12 months)2
- Downloads (Last 6 weeks)0
Reflects downloads up to 02 Feb 2025
Other Metrics
Citations
View Options
Login options
Check if you have access through your login credentials or your institution to get full access on this article.
Sign in