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

Abstract:
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.
 [Fulltext PDF]   [Fulltext HTML]   [XML: Abstract + References]   [References]   [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

URL: http://scialert.net/abstract/?doi=jse.2014.152.168

 
COMMENT ON THIS PAPER
.