Subscribe Now Subscribe Today
Science Alert
FOLLOW US:     Facebook     Twitter
Curve Top
Journal of Software Engineering
  Year: 2014 | Volume: 8 | Issue: 3 | Page No.: 152-168
DOI: 10.3923/jse.2014.152.168
Facebook Twitter Digg Reddit Linkedin StumbleUpon E-mail
Quantitative Verification of Trustworthy Service Flow by Stochastic Model Checking
Yang Liu

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.
PDF Fulltext XML References Citation Report Citation
How to cite this article:

Yang Liu , 2014. Quantitative Verification of Trustworthy Service Flow by Stochastic Model Checking. Journal of Software Engineering, 8: 152-168.

DOI: 10.3923/jse.2014.152.168








Curve Bottom