|
|
 |
| |
|
|
|
A Novel Approach to Generate the Property for Web Service Verification from Threat-Driven Model |
|
|
|
PP: 657-664 |
|
|
|
Author(s) |
|
|
|
Yonghua Zhu,
Honghao Gao,
|
|
|
|
Abstract |
|
|
| Web service is considered as one of the most promising computing paradigms, which works as plugin mode to provide the
value-added applications in Service-Oriented Computing (SOC) and Service-Oriented Architecture (SOA). The general Web service
verification focuses on functionality and its termination, such as deadlock or livelock. However, it might not be able to help in accurately
understanding service behaviours because it lacks interaction verifications, especially temporal behaviours. To this point, automatically
generating proper temporal logic formulae of verification property is a primary and important task since the manual property generation
is time-consuming and error-prone. Thus, this paper proposes an approach extending UML as service threat-driven model to generate
the verification property, including the features of functionality, time constraints and probability during service interactions. First,
it introduces a scenario description tool, mainly Probabilistic Timed Live Sequence Chart (PTLSC), on which kinds of implication
threats are discussed, specifying the insecure behaviours which should be prohibited from occurring in Web service. Second, it gives
corresponding transformation methods to extract the verification property from threat-driven model, in which the message coverage
criterion and partial relation are employed. These formulae are in the form of Probabilistic Timed Computation Tree Logic (PTCTL),
which afford an underlying guideline to guarantee the correctness and reliability of Web service since its threat-carried characteristics. |
|
|
|
|
|
|
|
