Semantic model checking security requirements for web services

Model checking is a formal verification method widely accepted in the web service world because of its capability to reason about service behaviors, at their process-level. It has been used as basic tool in several scenarios as service selection, service validation, and service composition. Furthermore, it has been widely applied to problems of security verification. The importance of semantics is widely recognized, as well. Indeed, there exists several solutions to the problem of providing semantics to web services, most of them relies on some form of Description Logic. This paper presents an integration of model checking and semantic reasoning technologies in an efficient way. This can be considered the first step towards the usage of semantic model checking in problems of security verification. The approach relies on a representation of services at the process level that is based on semantically annotated state transition systems (ASTS) and a representation of specifications ...

• Type: Journal
• Year: 2010
• Where: IEEEHPCS
• Authors: L. Boaro, E. Glorio, Francesco Pagliarecci, Luca Spalazzi
• Keywords: Applied Computing, Checking, IEEEHPCS 2010, Semantic, Semantic Reasoning