Parallel computation of the reachability graph of petri net models with semantic information

Summary Formal verification plays a crucial role when dealing with correctness of systems. In a previous work, the authors proposed a class of models, the Unary Resource Description Framework Petri Nets (U‐RDF‐PN), which integrated Petri nets and (RDF‐based) semantic information. The work also propo...

Full description

Saved in:
Bibliographic Details
Published in:Software, practice & experience practice & experience, 2017-05, Vol.47 (5), p.647-668
Main Authors: González‐López de Murillas, Eduardo, Fabra, Javier, Álvarez, Pedro, Ezpeleta, Joaquín
Format: Article
Language:English
Subjects:
Behavioural
cloud computing
Clouds
Computation
Graphs
high‐perfomance computing
Mathematical models
parallel computing
Petri nets
reachability graph
Semantics
Tasks
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary:Summary Formal verification plays a crucial role when dealing with correctness of systems. In a previous work, the authors proposed a class of models, the Unary Resource Description Framework Petri Nets (U‐RDF‐PN), which integrated Petri nets and (RDF‐based) semantic information. The work also proposed a model checking approach for the analysis of system behavioural properties that made use of the net reachability graph. Computing such a graph, specially when dealing with high‐level structures as RDF graphs, is a very expensive task that must be considered. This paper describes the development of a parallel solution for the computation of the reachability graph of U‐RDF‐PN models. Besides that, the paper presents some experimental results when the tool was deployed in cluster and cloud frameworks. The results not only show the improvement in the total time required for computing the graph, but also the high scalability of the solution, which make it very useful thanks to the current (and future) availability of cloud infrastructures. Copyright © 2016 John Wiley & Sons, Ltd.
ISSN:0038-0644
1097-024X
DOI:10.1002/spe.2438