Welcome to the InfoSci Platform
Mapping OWL-S Process Model to Timed Automata: A Model-Checking Timed Temporal Logic Oriented Approach

Mapping OWL-S Process Model to Timed Automata: A Model-Checking Timed Temporal Logic Oriented Approach

Amel Boumaza, Ramdane Maamri
Copyright: © 2018 |Volume: 11 |Issue: 1 |Pages: 20
ISSN: 1938-7857|EISSN: 1938-7865|EISBN13: 9781522543206|DOI: 10.4018/JITR.2018010103
Cite Article Cite Article

MLA

Boumaza, Amel, and Ramdane Maamri. "Mapping OWL-S Process Model to Timed Automata: A Model-Checking Timed Temporal Logic Oriented Approach." JITR vol.11, no.1 2018: pp.29-48. http://doi.org/10.4018/JITR.2018010103

APA

Boumaza, A. & Maamri, R. (2018). Mapping OWL-S Process Model to Timed Automata: A Model-Checking Timed Temporal Logic Oriented Approach. Journal of Information Technology Research (JITR), 11(1), 29-48. http://doi.org/10.4018/JITR.2018010103

Chicago

Boumaza, Amel, and Ramdane Maamri. "Mapping OWL-S Process Model to Timed Automata: A Model-Checking Timed Temporal Logic Oriented Approach," Journal of Information Technology Research (JITR) 11, no.1: 29-48. http://doi.org/10.4018/JITR.2018010103

Export Reference

Mendeley
Favorite Full-Issue Download

Abstract

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.

Request Access

You do not own this content. Please login to recommend this title to your institution's librarian or purchase it from the IGI Global bookstore.