Quantitative verification of trustworthy service flow by stochastic model checking

被引：0

作者：

Liu, Yang ^{[1
,2
]}

机构：

[1] School of Information Science and Technology, Taishan University, Taian, Shandong

[2] Laboratory for Novel Software Technology, Nanjing University, Nanjing, 210093, Jiangsu

来源：

Journal of Software Engineering | 2014年 / 8卷 / 03期

关键词：

Formal semantics; Nondeterministic probabilistic p etri net; Stochastic model checking; Trustworthy service flow;

D O I：

10.3923/jse.2014.152.168

中图分类号：

学科分类号：

摘要：

Trustworthy Service Flow (TSF) is one of the most representative paradigm for trustworthy Software. Because TSF involves the non-functional attribute, such as quality of service and trustworthiness, the modelling and verification of which is very difficult. It is not sufficient to meet the TSF requirements just using the classical model checking. This paper propose a method to quantitative verification of TSF with stochastic model checking. Firstly, based on the extension of OWL-S upper ontology, the formal semantics for TSF is presented by Nondeterministic Probabilistic Petri Net (NPPN) and the translation process of which is implemented automatically. Moreover, the simplification rules for NPPN and is also presented. Then, the new temporal logic as PCTL is proposed for specifying the properties of TSF and the stochastic model checking algorithm is put forward for quantitative verification TSF. The feasibility and effectiveness of the method are illustrated by the available service flow case. © 2014 AcademicJournals Inc.

引用

页码：152 / 168

页数：16

共 24 条

[1]

Albanese M., Chellappa R., Moscato V., Picariello A., Subrahmanian Y.S., Turaga P., Udrea O., A constrained probabilistic petri net framework for human activity detection in video, IEEE Trans. Multimedia, 10, pp. 1429-1443, (2008)

[2]

Berners-lee T., Hendler J., Lassila O., The semantic web, (2001)

[3]

Calinescu R., Grunske L., Kwiatkowska M., Mirandola R., Tamburrelli G., Dynamic QoS management and optimization in service-based systems, IEEE Trans. Software Eng., 37, pp. 387-409, (2011)

[4]

Caliz E., Umapathy K., Sanchez-ruiz A.J., Elfayoumy S.A., Analyzing web service choreography specifications using colored Petri nets, Proceedings of the 6th International Conference on Service-Oriented Perspectives in Design Science Research, pp. 412-426, (2011)

[5]

Cardoso J., Sheth A., Miller J., Arnold J., Kochut K., Quality of service for workflows and web service processes, Web Semantics, 1, pp. 281-308, (2004)

[6]

Curbera F., Khalaf R., Mukhi N., Tai S., Weerawarana S., The next step in web services, Commun. ACM, 46, pp. 29-34, (2003)

[7]

Dai Y., Yang L., Zhang B., QoS-driven self-healing web service composition based on performance prediction, J. Comput. Sci. Technol., 24, pp. 250-261, (2009)

[8]

Fan X.Q., Jiang C.J., Wang J.L., Pang S.C., Random-QoS-aware reliable web service composition, J. Software, 20, pp. 546-556, (2009)

[9]

Hansson H., Jonsson B., A logic for reasoning about time and reliability, Formal Aspects Comput., 6, pp. 512-535, (1994)

[10]

Kudlek M., Probability in petri nets, Fundam. Inform., 67, pp. 121-130, (2005)

← 1 2 3 →