{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T17:14:36Z","timestamp":1654103676211},"reference-count":12,"publisher":"IGI Global","issue":"2","content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2015,4,1]]},"abstract":"<p>Service oriented software systems running in a highly open, dynamic and unpredictable Internet environment are inevitable to face all kinds of uncertainty. To monitor the operation of the web services system behavior analysis and analysis whether the system behavior is consistent with the requirements is the basis to determine whether the system needs to be reconfigured. In this paper, an analytical platform for the behavior of a web service-oriented system based on the probabilistic model checking is introduced which provides the basis for judging whether a system needs to be reconfigured by applying the approach of probabilistic model checking to verify whether the behavior system model is satisfied requirement properties. This platform is implemented in Java language and using the dot tool that the Graphviz provides and the PRISM model checker to construct the behavior model of the web service-oriented system based on web log files, to view and edit behavior models visually, and to convert the model from one form to another to make it convenience for users to use the model checker PRISM. Finally, we can judge whether the model is satisfied the desired requirements according to the verification result.<\/p>","DOI":"10.4018\/ijsi.2015040104","type":"journal-article","created":{"date-parts":[[2015,1,30]],"date-time":"2015-01-30T19:26:06Z","timestamp":1422645966000},"page":"24-38","source":"Crossref","is-referenced-by-count":5,"title":["A Platform for Analyzing Behaviors of Service-Oriented Application Based on the Probabilistic Model Checking"],"prefix":"10.4018","volume":"3","author":[{"given":"Jinyu","family":"Kai","sequence":"first","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai, P.R. China & Shanghai Key Laboratory of Computer Software Evaluating and Testing, Shanghai, P.R. China"}]},{"given":"Huaikou","family":"Miao","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai, P.R. China & Shanghai Key Laboratory of Computer Software Evaluating and Testing, Shanghai, P.R. China"}]},{"given":"Kun","family":"Zhao","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai, P.R. China"}]},{"given":"Jiaan","family":"Zhou","sequence":"additional","affiliation":[{"name":"School of Computer Engineering and Science, Shanghai University, Shanghai, P.R. China"}]},{"given":"Honghao","family":"Gao","sequence":"additional","affiliation":[{"name":"Computing Center, Shanghai University, Shanghai, P.R. China"}]}],"member":"2432","reference":[{"key":"ijsi.2015040104-0","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60045-0_48"},{"issue":"6","key":"ijsi.2015040104-1","first-page":"388","article-title":"Modular verification of software components in C. Software Engineering","volume":"30","author":"S.Chaki","year":"2004","journal-title":"IEEE Transactions on"},{"key":"ijsi.2015040104-2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58043-3_19"},{"key":"ijsi.2015040104-3","author":"E. M.Clarke","year":"1999","journal-title":"Model checking"},{"key":"ijsi.2015040104-4","doi-asserted-by":"crossref","unstructured":"D\u2019Argenio, P. R., Jeannet, B., Jensen, H. E., & Larsen, K. G. (2002). Reduction and refinement strategies for probabilistic analysis. In Process Algebra and Probabilistic Methods: Performance Modeling and Verification (pp. 57-76). Springer Berlin Heidelberg.","DOI":"10.1007\/3-540-45605-8_5"},{"key":"ijsi.2015040104-5","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-18638-7_6"},{"key":"ijsi.2015040104-6","doi-asserted-by":"publisher","DOI":"10.1007\/BF01211866"},{"key":"ijsi.2015040104-7","doi-asserted-by":"publisher","DOI":"10.1145\/1530873.1530882"},{"key":"ijsi.2015040104-8","unstructured":"Parker, D. A. (2002). Implementation of symbolic model checking for probabilistic systems. Doctoral dissertation, University of Birmingham."},{"key":"ijsi.2015040104-9","author":"M. L.Puterman","year":"2009","journal-title":"Markov decision processes: discrete stochastic dynamic programming"},{"key":"ijsi.2015040104-10","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60218-6_17"},{"key":"ijsi.2015040104-11","doi-asserted-by":"publisher","DOI":"10.1145\/1592434.1592436"}],"container-title":["International Journal of Software Innovation"],"original-title":[],"language":"ng","link":[{"URL":"https:\/\/www.igi-global.com\/viewtitle.aspx?TitleId=122791","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,6,1]],"date-time":"2022-06-01T16:44:37Z","timestamp":1654101877000},"score":1,"resource":{"primary":{"URL":"https:\/\/services.igi-global.com\/resolvedoi\/resolve.aspx?doi=10.4018\/ijsi.2015040104"}},"subtitle":[""],"short-title":[],"issued":{"date-parts":[[2015,4,1]]},"references-count":12,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2015,4]]}},"URL":"https:\/\/doi.org\/10.4018\/ijsi.2015040104","relation":{},"ISSN":["2166-7160","2166-7179"],"issn-type":[{"value":"2166-7160","type":"print"},{"value":"2166-7179","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,4,1]]}}}