A new framework for the verification of service trust behaviors

We propose in this paper a model checking framework for service trust behaviors. We devise a new trust behavior model, which is a deterministic PushDown Automaton (PDA) based trust behavior model. This model is built based on the observations’ sequences, which are derived from the interactions with...

Full description

Saved in:
Bibliographic Details
Published in:Knowledge-based systems 2017-04, Vol.121, p.7-22
Main Authors: El-Qurna, Jumana, Yahyaoui, Hamdi, Almulla, Mohamed
Format: Article
Language:English
Subjects:
Algorithms
Fixed-point Logic with Chop
Model checking
Pushdown automata
Service
Trust
Trust behaviors
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:We propose in this paper a model checking framework for service trust behaviors. We devise a new trust behavior model, which is a deterministic PushDown Automaton (PDA) based trust behavior model. This model is built based on the observations’ sequences, which are derived from the interactions with services. Furthermore, we express the regular and non-regular trust behavior properties using Fixed point Logic with Chop (FLC). The model checking of service trust behaviors with respect to trust properties is performed using a symbolic FLC model checking algorithm. Finally, we present some experiments to assess the efficiency of the proposed algorithm.
ISSN:0950-7051
1872-7409
DOI:10.1016/j.knosys.2017.01.011