COMBAS: A Semantic-Based Model Checking Framework

Abstract—The introduction of semantic aspects in scientific workflows is a powerful approach that allows the analysis of the workflow prior to its development and deployment. In this paper, the COMBAS framework for the semantic-based model checking processing is presented. COMBAS integrates the required languages and tools and implements its own algorithms in order to allow the verification of properties on a model specified with the U-RDF-PN formalism, a high-level Petri net-based formalism, which introduces parametric semantic annotations in the model. COMBAS facilitates the generation of temporal logic formulae to express the properties that are going to be verified in the model as well as it provides system designers with an RDF and CTL adapted environment to browse and review the results. The suitability of the proposed framework is demonstrated by means of its application to the analysis of the EBI InterProScan scientific workflow