WUppaal: A web-service for the Uppaal model-checker

Author(s):  
Peter Fogh ◽  
Thomas C. Hald ◽  
Brian Nielsen
Keyword(s):  
2015 ◽  
Vol 3 (2) ◽  
pp. 24-38 ◽  
Author(s):  
Jinyu Kai ◽  
Huaikou Miao ◽  
Kun Zhao ◽  
Jiaan Zhou ◽  
Honghao Gao

Service oriented software systems running in a highly open, dynamic and unpredictable Internet environment are inevitable to face all kinds of uncertainty. To monitor the operation of the web services system behavior analysis and analysis whether the system behavior is consistent with the requirements is the basis to determine whether the system needs to be reconfigured. In this paper, an analytical platform for the behavior of a web service-oriented system based on the probabilistic model checking is introduced which provides the basis for judging whether a system needs to be reconfigured by applying the approach of probabilistic model checking to verify whether the behavior system model is satisfied requirement properties. This platform is implemented in Java language and using the dot tool that the Graphviz provides and the PRISM model checker to construct the behavior model of the web service-oriented system based on web log files, to view and edit behavior models visually, and to convert the model from one form to another to make it convenience for users to use the model checker PRISM. Finally, we can judge whether the model is satisfied the desired requirements according to the verification result.


Author(s):  
Anas Abou El Kalam ◽  
Yves Deswarte

With the emergence of Web Services-based collaborative systems, new issues arise, in particular those related to security. In this context, Web Service access control should be studied, specified and enforced. This work proposes a new access control framework for Inter-Organizational Web Services: “PolyOr- BAC”. On the one hand, the authors extend OrBAC (Organization-Based Access Control Model) to specify rules for intra- as well as inter-organization access control; on the other hand, they enforce these rules by applying access control mechanisms dedicated to Web Services. Furthermore, the authors propose a runtime model checker for the interactions between collaborating organizations, to verify their compliance with previously signed contracts. In this respect, not only their security framework handles secure local and remote accesses, but also deals with competition and mutual suspicion between organizations, controls the Web Service workflows and audits the different interactions. In particular, every deviation from the signed contracts triggers an alarm, the concerned parties are notified, and audits can be used as evidence for a judge to sanction the party responsible for the deviation.


2011 ◽  
pp. 537-557
Author(s):  
Anas Abou El Kalam ◽  
Yves Deswarte

With the emergence of Web Services-based collaborative systems, new issues arise, in particular those related to security. In this context, Web Service access control should be studied, specified and enforced. This work proposes a new access control framework for Inter-Organizational Web Services: “PolyOr- BAC”. On the one hand, the authors extend OrBAC (Organization-Based Access Control Model) to specify rules for intra- as well as inter-organization access control; on the other hand, they enforce these rules by applying access control mechanisms dedicated to Web Services. Furthermore, the authors propose a runtime model checker for the interactions between collaborating organizations, to verify their compliance with previously signed contracts. In this respect, not only their security framework handles secure local and remote accesses, but also deals with competition and mutual suspicion between organizations, controls the Web Service workflows and audits the different interactions. In particular, every deviation from the signed contracts triggers an alarm, the concerned parties are notified, and audits can be used as evidence for a judge to sanction the party responsible for the deviation.


2015 ◽  
pp. 831-844
Author(s):  
Jinyu Kai ◽  
Huaikou Miao ◽  
Kun Zhao ◽  
Jiaan Zhou ◽  
Honghao Gao

Service oriented software systems running in a highly open, dynamic and unpredictable Internet environment are inevitable to face all kinds of uncertainty. To monitor the operation of the web services system behavior analysis and analysis whether the system behavior is consistent with the requirements is the basis to determine whether the system needs to be reconfigured. In this paper, an analytical platform for the behavior of a web service-oriented system based on the probabilistic model checking is introduced which provides the basis for judging whether a system needs to be reconfigured by applying the approach of probabilistic model checking to verify whether the behavior system model is satisfied requirement properties. This platform is implemented in Java language and using the dot tool that the Graphviz provides and the PRISM model checker to construct the behavior model of the web service-oriented system based on web log files, to view and edit behavior models visually, and to convert the model from one form to another to make it convenience for users to use the model checker PRISM. Finally, we can judge whether the model is satisfied the desired requirements according to the verification result.


Author(s):  
Xiaohong Li ◽  
Jiayi Xu ◽  
Guangquan Xu ◽  
Jianye Hao ◽  
Xiaoru Li ◽  
...  

Ensuring the fairness and non-repudiation in the security exchange protocol of web service is critical. Model checking is often used for automatic verification for the security properties of protocol. However, the current model checker tools cannot support formalizing protocols with cryptographic primitives, specifying properties with linear temporal logic (LTL) and automatically generating resilient intruder model simultaneously and the application range of them is severely limited. To solve this problem, a model checker Fepchecker is proposed to verify the fairness and non-repudiation properties, which are critical features in security exchange protocols. Firstly, applied pi-calculus is extended to specify the protocols, and the LTL assertion is used for precisely describing fairness and non-repudiation. Secondly, an intruder model is applied to construct their behavior sequences automatically and the protocol sessions and message pattern are used to alleviate the states explosion problem. Thirdly, in our model checking algorithm, the fairness and non-repudiation properties are verified based on Labeled Transition System (LTS) semantics model and the MakeOneMove method is used to explore the state space on-the-fly in the verification process. Finally, Fepchecker is applied to verify six representative protocols and the results show that Fepchecker can effectively verify their fairness and non-repudiation properties.


2013 ◽  
Vol 791-793 ◽  
pp. 1581-1584
Author(s):  
Xiao Bo Yang

In order to generate the realization model of business process quickly, a method of formalize model is proposed which based on Web service choreography language in this paper. The specific studying process is as follows. Firstly, several Web services choreography language and its characteristics are introduced, and then analyzed the natural projection and expansion model of service choreography, finally, model checker SPIN is used to simulate and verify the service choreography. The result shows that the succinct service choreography language can create Web service choreography model efficiently, and through the projection rules, which can better meet the needs of the business process implementation.


2013 ◽  
Vol 5 (1) ◽  
pp. 41-54 ◽  
Author(s):  
Wael Sellami ◽  
Hatem Hadj Kacem ◽  
Ahmed Hadj Kacem

A web service composition is considered as a real revolution in SOA (Service Oriented Architecture). It is based on assembling independent and loosely coupled services to build a composed web service. This composition can be described from both a local or a global perspective by respective orchestration or choreography. The validation of web service orchestrations is the main topic of this work. It is based on the verification of two classes of properties: generic and specific properties. The former can be checked for any invoked web services whereas the specific properties are different interdependence relationships between activities within an orchestration process. These properties cannot be directly verified on the orchestration process, so, the authors have to use formal techniques. In this paper, they propose a formal approach for the validation of web service orchestrations. This work adopts WS-BPEL 2.0 as the language to describe the web service orchestration and uses the SPIN model-checker for the verification engine. The WS-BPEL specification is translated into Promela code which is the input language for the SPIN model-checker, in order to check generic and specific properties expressed with LTL (Linear Temporal Logic).


2005 ◽  
Vol 8 (1) ◽  
pp. 16-18
Author(s):  
Howard F. Wilson
Keyword(s):  

Sign in / Sign up

Export Citation Format

Share Document