Find research datasets worth reusing
Search datasets from major research repositories and use ShareScore to quickly assess how well each record supports discovery, access, and reuse.
8
datasets available to search
ShareScore release 0.9.0
Dataset results
8 results for “Petri nets”
An introduction to the use of Extended Petri Nets to represent Hydrological Dynamical Systems
<p>The video tries to be a quiet introduction to the Extended Petri Nets (EPN), a graphical representations designed to describe Earth Science and Environmental models that results is systems of ordinary differential equations. The video uses an example to exemplify the mechanics of EPN and constitute ancillary material for a paper submitted to Hydrological Processes (https://osf.io/fpx7y/). The main reference for the EPN is: Bancheri,M., Serafin,F. and Rigon, R (2019), "The representation of hydrological dynamical systems using the extended petri nets." Water Resources Research, 8(01), 159–27. In our opinion, EPN improve models representation and help to understand the feedbacks among the various processes.</p> <p> </p>
Automatic message sequence chart creation from simulation run of the parametric colored Petri net model of the Chandy-Lamport algorithm with four processes
<p><span>The video shows the creation of the message sequence chart from a simulation run of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm using the CPN tool with four constituting processes. The picture shows the resulting message sequence chart. </span></p> <p><strong><span>Message Sequence Chart of Parametric Model With 4 Processes via Automatic Simulation Run_SuppInfo.mp4</span></strong><span>: This video shows the automatic generation of a message sequence chart of the proposed parametric colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.0. The model's number of constituting processes is parametric and was set to four. The video was generated using the authors' updated CPN tool extension server. The automatic simulation run of the model has been used to create this video. The CPN tool randomly selects the enabled transition at each step in an automatic simulation run.</span></p> <p><strong><span>Picture of Message Sequence Chart of Parametric Model With 4 Processes_SuppInfo.png:</span></strong><span> This picture shows the automatically generated message sequence chart of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm that is visible in the above video clip. The number of constituting processes was set to four. </span></p>
Automatic message sequence chart creation from simulation run of the Chandy-Lamport algorithm modeled by colored Petri net
<p>Videos of two message sequence chart creation from simulation runs of the Chandy-Lamport algorithm modeled by colored Petri net using the CPN tool.</p> <p><strong>Message Sequence Chart Of Model With Automatic Simulation Run_SuppInfo.mp4</strong>: This video shows the automatic generation of a message sequence chart of a proposed colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.1. The video has been generated by the authors' updated extension server of the CPN tool. The automatic simulation run of the model has been used to create this video. The CPN tool randomly selects the enabled transition in an automatic simulation run.</p> <p><strong>Message Sequence Chart Of Model With Step-By-Step Simulation Run_SuppInfo.mp4:</strong> This video shows the automatic generation of a message sequence chart of the proposed colored Petri net model of the Chandy-Lamport algorithm in a step-by-step simulation run with our updated extension server of the CPN tools version 4.0.1. We fired our selected enabled transition of the model to create this video.</p>
Model checking of Chandy-Lamport algorithm modeled by colored Petri net
<p>This video shows model checking of a proposed colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.1. It shows the functions and codes written in ML language and the result of calling them used for model checking the proposed model's state space graph. The last ML code at the end of the page, named state space, does whole model checking and operates using previously displayed codes and functions. This video aimed to demonstrate the steps of our proposed model checking.</p>
Benchmark Petri Net Models Used for the Evaluation of B-I-Sat
<p>Collection and documentation of the benchmark Petri net models used for the evaluation of the B-I-Sat algorithm.</p>
Model checking of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm
<p>This video shows model checking of a proposed parametric colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.0. The number of constituting processes is parametric in this model. It shows the functions written in ML language and the result of calling them for customized analysis of the proposed model's state space graph. The last ML code at the end of the page, "state space," summarizes the model checking and operates by calling previously displayed functions. This video aimed to demonstrate the proposed verification process of the parametric model.</p>
Automatic message sequence chart creation from simulation run of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm
<p><span>These videos show the creation of two message sequence charts from simulation runs of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm using the CPN tool with three constituting processes. </span></p> <p><strong><span>Message Sequence Chart of <span> </span>Parametric Model With 3 Processes via Automatic Simulation Run_SuppInfo.mp4</span></strong><span>: This video shows the automatic generation of a message sequence chart of the proposed parametric colored Petri net model of the Chandy-Lamport distributed global snapshot algorithm using the CPN tool version 4.0.0. The number of constituting processes is parametric in the model and was set to three. The video was generated using the authors' updated CPN tool extension server. The automatic simulation run of the model has been used to create this video. The CPN tool randomly selects the enabled transition at each step in an automatic simulation run.</span></p> <p><strong><span>Message Sequence Chart of Parametric Model With 3 Processes via Step-By-Step Simulation Run_SuppInfo.mp4:</span></strong><span> This video shows the automatic generation of a message sequence chart of the proposed parametric colored Petri net model of the Chandy-Lamport algorithm in a step-by-step simulation run with our updated extension server of the CPN tools version 4.0.0. The number of constituting processes is parametric in the model and was set to three. We manually fired our selected enabled transition of the model to create this video. </span></p>
A Petri net tool for software performance estimation based on upper throughput bounds
<p>Functional and non-functional properties analysis (i.e., dependability, security, or performance) ensures that requirements are fulfilled during the design phase of software systems. However, the Unified Modelling Language (UML), standard <em>de facto</em> in industry for software systems modelling, is unsuitable for any kind of analysis but can be tailored for specific analysis purposes through profiling. For instance, the MARTE profile enables to annotate performance data within UML models that can be later transformed to formal models (e.g., Petri nets or timed automatas) for performance evaluation. A performance (or throughput) estimation in such models normally relies on a whole exploration of the state space, which becomes unfeasible for large systems. To overcome this issue upper throughput bounds are computed, which provide an approximation to the real system throughput with a good complexity-accuracy trade-off. This paper introduces a tool, namedPeabraiN, that estimates the performance of software systems via their UML models. To do so, UML models are transformed to Petri nets where performance is estimated based on upper throughput bounds computation. PeabraiN also allows to compute other features on Petri nets, such as the computation of upper and lower marking place bounds, and to simulate using an approximate (continuous) method. We show the applicability of PeabraiN by evaluating the performance of a building closed circuit TV system.</p>
ScienceDex guides
Understand access before you commit
These curated guides explain access requirements, typical timelines, costs, and reuse considerations for widely used research datasets.
Allen Brain Atlas
Allen Brain Atlas is an Allen Institute collection of brain map atlases, datasets, APIs, and analysis tools covering mouse, human, and non-human primate brain resources.
Annotated Behaviour and Observability Dataset (ABODe)
ABODe is a University of Edinburgh DataShare dataset for behavior classification in group-housed mice using home-cage video, identities, bounding boxes, ground-plate positions, and annotator labels.
DANDI Archive for NWB datasets
DANDI is a BRAIN Initiative archive for publishing and sharing neurophysiology data, including electrophysiology, optophysiology, and behavioral data packaged as NWB and related standards.
International Brain Laboratory public data
The International Brain Laboratory public data releases expose standardized mouse decision-making experiments, including Neuropixels recordings, widefield calcium imaging, behavior, and session metadata accessed through the ONE API.
OpenNeuro
OpenNeuro is a free, open platform for sharing neuroimaging datasets, with public search, dataset pages, and download paths for web, S3, DataLad, and the OpenNeuro CLI.