Mapping OWL-S Process Model to Timed Automata

2018 ◽  
Vol 11 (1) ◽  
pp. 29-48
Author(s):  
Amel Boumaza ◽  
Ramdane Maamri
Keyword(s):  
Web Services ◽  
Process Model ◽  
Timed Automata ◽  
Automatic Verification ◽  
Covering Problems ◽  
Field Verification ◽  
Starting Point ◽  
Quantitative Properties ◽  
Time Systems

The conversion of web services to semantic web comes the opportunity to automate various tasks. OWL-S plays a key role in describing web services behaviour. While ontology-based semantics given to OWL-S is structural rather than behaviourally oriented, we cannot automate an essential task in this field, verification. In this article, the mapping of OWL-S process model to Timed automata is investigated, which is a suitable formalism for real time systems modeling and automatic verification. Hence, this has led to not only enabling automatic verification but also covering problems related to automated verification of temporal quantitative properties as bounded liveness property. As a starting point, the OWL-S and sub entry of time ontologies for describing the timed behaviour of services has been chosen. A defined set of mapping rules is used to automatically encode control constructs defined in OWL-S and temporal information into timed automata. Also, it is shown how a Uppaal checker is used to check required properties formulated in TCTL. Finally, an EClinic case study is used to illustrate the technique.

A Model-based Approach for Diagnosing Fault in Web Service Processes

2013 ◽  
pp. 92-116
Author(s):  
Yuhong Yan ◽  
Philippe Dague ◽  
Yannick Pencolé ◽  
Marie-Odile Cordier
Keyword(s):  
Web Services ◽  
Web Service ◽  
Business Process ◽  
Business Processes ◽  
Formal Model ◽  
Service Orchestration ◽  
Model Based ◽  
Architecture Framework ◽  
Web Service Orchestration ◽  
Business Process Execution

Web services based on a service-oriented architecture framework provide a suitable technical foundation for business process management and integration. A business process can be composed of a set of Web services that belong to different companies and interact with each other by sending messages. Web service orchestration languages are defined by standard organizations to describe business processes composed of Web services. A business process can fail for many reasons, such as faulty Web services or mismatching messages. It is important to find out which Web services are responsible for a failed business process because we could penalize these Web services and exclude them from the business process in the future. In this paper, we propose a model-based approach to diagnose the faults in a Web service-composed business process. We convert a Web service orchestration language, more specifically BPEL4WS, into synchronized automata, so that we have a formal description of the topology and variable dependency of the business process. After an exception is thrown, the diagnoser can calculate the business process execution trajectory based on the formal model and the observed evolution of the business process. The faulty Web services are deduced from the variable dependency on the execution trajectory. We demonstrate our diagnosis technique with an example.

Tweaking the Odds in Probabilistic Timed Automata

2021 ◽  
pp. 39-58
Author(s):  
Arnd Hartmanns ◽  
Joost-Pieter Katoen ◽  
Bram Kohlen ◽  
Jip Spel
Keyword(s):  
Timed Automata ◽  
Probabilistic Timed Automata

Enhancement of a Fault Measure for AMSs Using Probabilistic Timed Automata

2011 ◽  
Vol 317-319 ◽  
pp. 681-684
Author(s):  
Yi Sheng Huang ◽  
Ho Shan Chiang
Keyword(s):  
Probability Distribution ◽  
Working Conditions ◽  
Timed Automata ◽  
Probabilistic Automata ◽  
Discrete Probability ◽  
Novel Approach ◽  
Reasoning Strategy ◽  
Real Value ◽  
Target States ◽  
Probabilistic Timed Automata

A novel approach for probabilistic timed structure that is based on combining the formalisms of timed automata and probabilistic automata representation of the system is proposed. Due to their real-valued clocks can measure the passage of time and transitions can be probabilistic such that it can be expressed as a discrete probability distribution on the set of target states. The usage of clock variables and the specification of state space are illustrated with real value time applications. The transitions between states are probabilistic by events which describe either the occurrence of faults or normal working conditions. Additionally, the passage of discrete time and transitions can be probabilistic by mean of the theory of expectation sets to obtain a unified measure reasoning strategy.

Sign in / Sign up

Export Citation Format

Share Document