Distinguishing Automata Machine By Using UPPAAL As A Model Checker
Yogeswaran Nagarathinam, Dr. Nor Fazlida Mohd Sani
Index Terms: model checking, electronic payment, Finite State Automata, Non Deterministic Pushdown Automata, UPPAAL, Online Shopping system, possible traces .
Abstract: Upon to the evolvement of technologies, electronic commerce and other online businesses are exposed to vulnerability hence invoking damages and untraceable fraud to the end users. Software engineers in the moment by moment, tracks the design and the analysis so that they can ensure the safety of the overall process from the root itself. Besides that we have proposed model checking to check on the behavior of a design. Thus our research has identified and differentiate the best of two methods of model checking which is Finite State Automata and Non Deterministic Pushdown automata. For the purpose of simulation, UPPAAL tool has been used over a part of Online Shopping system case study.
. Esparza, J., Hansel, D. Rossmanith, P.Schwoon, S.: Efficient Algorithms for model checking Pushdown Systems. In: Emerson, E.A., Sistla, A.P.(eds.) CAV 2000.LNHC, vol.1855, pp. 232-247. Springer, Heidelberg (2000)
. Jia Mei., Huaikou Miao, Qingguo Xu, Pan Liu, : Modeling and Verifying Web Service Applications with time Constraints. School of Computer Engineering and Science and Shanghai Key Laboratory of Computer Software Evaluating & Testing, Shangai, China, 978-0-7695-4147-1/10 IEEE China (2010)
. Deepak Arora., Bramah Hazela, Vipin Saxena, : Semantics for UML Model Transformation and Generation of Regular Grammar. Department of Computer Science & Engineering Amity University, Lucknow, India,http://doi.acm.org/10.1145/180921.2180931 ACM (May 2012)
. Wenfei Fan., Floris Geerts, Wouter Gelade, Frank Neven, Antonella Poggi,: Complexity and Composition of Synthesized Web Services. University of Edinburgh & Bell Labs, PODS’08 , June 9 – 12,2008, Vancouver, BC , Canada ACM (2008)
. Afef Jmal Maalej., Moez Krichen, Mohamed Jmaiel,: WSCCT : A Tool for WS-BPEL Compositions Conformance Testing. ReDCAD Laboratory, University of Sfax Edinburgh & Bell Labs, ACM ( March 2013 )
. Jocelyn Simmonds., Yuan Gan, Marsha Chechik, Shiva, Bill O’Farell, Elena Litani, Julie Waterhouse,: Runtime Monitoring of Web Service Conversations , IEEE Transaction on Services Computing Vol.2.No.3 (July – Sept 2013 )
. Hamidreza Amouzegar.,Shahriar Mohammadi, Mohammad Jaafar Tarokh, Anahita Naghilouye Hidaji,: A New Approach on Interactive SOA Security Model Based on Automata , Seventh IEEE/ACIS International Conference Computer and Information Science, 978-0-7695-3131-1/08 (2008)
. Cagdas Evren Gerede.,Richard Hull, Oscar H.Ibarra, Jianwen Su,: Automated Composition of E-services: Lookaheads, University of California, New York USA, 1-58113-871-7/04/0011 (2004)
. Qi He.,: Recognizing valid artifacts business processes: School of Computer Science , Fudan, China, International Conference on Web Intelligent and intelligent Agent Technology, IEEE 978-0-7695-4880-7/12 (2012)
. Alex Thom., S.Venkatesh: Rewriting of Visibly Pushdown Languages for XML Data Integration: Department of Computer Science, University of Victoria School of Computer Science , Napa Valley, California, USA, ACM 978-1-59593-991-3/08/10 (2008)
. G.D’iaz., K.Larsen, J.Pardo, F.Cuartero, V.Valero,: An Approach to handle Real Time and Probabilistic behaviors in e commerce : Validating the SET Protocol Rewriting of Visibly Pushdown Languages for XML Data Integration: Department of Computer Science, University of CastillaLa, SantaFe, New Mexico, USA, ACM 1581139640 (2005)