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.
42
datasets available to search
ShareScore release 0.9.0
Dataset results
42 results for “model checking”
Models and Infrastructure used in "Deep Statistical Model Checking"
<p>This repository contains the models and all other infrastructure (learning procedure, NNs, Jani generator, maps, modes & mcsta binaries) used in the FORTE 2020 paper "Deep Statistical Model Checking".</p>
Logical model for Model checking to assess T-helper cell plasticity
<p>Logical modeling has proven suitable for the dynamical analysis of large signaling and transcriptional regulatory networks. In this context, signaling input components are generally meant to convey external stimuli, or environmental cues. In response to such external signals, cells acquire specific gene expression patterns modeled in terms of attractors (e.g. stable states). The capacity for cells to alter or reprogram their differentiated states upon changes in environmental conditions is referred to as cell plasticity.</p> <p>In <a href="https://dx.doi.org/10.3389/fbioe.2014.00086">[1]</a>, it is presented an extended version of a published logical model of T-helper cell differentiation and plasticity, which accounts for novel cellular subtypes. The model encompasses 20 signaling pathways, a dozen of transcription factors, and about 30 cytokines, amounting to 101 components in total.</p> <p>Computational methods recently developed to efficiently analyze large models <a href="http://ginsim.org/node/185#ref1">[1]</a> are first used to study static properties of the model (i.e. stables states). Symbolic model checking is then applied to get further insights into reachability properties between Th canonical subtypes upon changes of specific prototypic environmental cues.</p> <p>The model reproduces novel reported Th subtypes (Tfh, Th9, Th22) and predicts additional Th hybrid subtypes in term of stables states. Using the model checker NuSMV-ARCTL, an abstract view of the dynamics, called reprograming graph, is produced providing a global and synthetic view of Th plasticity. The model is consistent with experimental data showing the polarization of naïve Th cells into the canonical Th subtypes. The model further predicts substancial plasticity of Th subtypes depending on the signalling environment.</p>
End-to-End Multimodal Fact-Checking and Explanation Generation: A Challenging Dataset and Models
<p>We propose the end-to-end multimodal fact-checking and explanation generation, where the input is a claim and a large collection of web sources, including articles, images, videos, and tweets, and the goal is to assess the truthfulness of the claim by retrieving relevant evidences and predicting a truthfulness label (i.e., support, refute and not enough information), and to generate a rationalization statement to explain the reasoning and ruling process. To support this research, we construct MOCHEG, a large-scale dataset consisting of 21,184 claims where each claim is annotated with a truthfulness label and ruling statement, with 43,148 text evidences and 15,373 image evidences. </p>
Experimental data for Distributed parametric model checking timed automata under non-Zenoness assumption
<p>This is the experimental data mentioned in the paper "Distributed parametric model checking timed automata under non-Zenoness assumption", published in FMSD (Formal Methods in System Design), 2022.</p> <p>Experiments were conducted using the distributed version of IMITATOR 2.9.2 (Butter Incaberry) on two Intel Xeon Silver 4114 at 2.2GHz (20 cores in total), and 96GiB of memory, running under Ubuntu 16.04 LTS 64-bit.</p>
A Tool for Collaborative Consistency Checking During Modeling (dataset)
<div>This dataset contains a few snapshots as well as the jar files for the tools (server and client).</div> <div> </div> <div>It also contains a image displayng the metamodel representation of the streamlined language (Metamodel-sUML) which is used to define the models created by our sUML modeler.</div> <div> </div> <div> </div> <div> </div> <div><strong>Running the tools:</strong></div> <div> </div> <div><strong><a href="https://isse.jku.at/designspace/index.php/Abstract_Rule_Language">Requirements</a></strong>: </div> <div>Windows 10/11</div> <div>JDK 21 or above</div> <div> </div> <div><strong>How to run the server and add rules:</strong></div> <ul> <li>Run the DesignSpace-Server</li> <li>On the top menu, click Consistency > Rule Editor </li> <li>To add a new rule, select a Language (sUMLv3) and an instance type (e.g., Class)</li> <li>Add a name for the rule</li> <li>Add a definition for the rule (use the ARL language (<a href="https://isse.jku.at/designspace/index.php/Abstract_Rule_Language">https://isse.jku.at/designspace/index.php/Abstract_Rule_Language</a>) and the properties of the UML metamodel</li> <li>Always click validate (if there are erros in the rule defintioj, check the log)</li> <li>If no erros are found, the rule is created.</li> </ul> <div><strong>Run the modeler tools:</strong></div> <ul> <li>When running an instance of the sUML-Modeler, you need to select a user (currently there are four users, more can be added using the DesignSpace server)</li> <li>To connect multiple tools, select different users (selecting the same user will close the previously connected tool as each user can only connect once)</li> <li>Always create a root model before adding other diagrams</li> <li>For changes to be sent to the server, select DesignSpace > Commit from the tool menu</li> <li>The option DesignSpace > Update will pull changes (in case they exist)</li> <li>To enable the highlighting of inconsistencies, select Validate > Display Inconsistencies</li> </ul> <div> </div> <div> </div> <div><strong>Sample rules:</strong></div> <div> </div> <div>Instance Type: class</div> <div>Name: A class must have unique operations</div> <div> </div> <div>self.operations->forAll(o1, o2 | o1 <> o2 implies o1.name <> o2.name)</div> <div> </div> <div>Instance Type: class</div> <div>Name: A class must have unique attributes</div> <div> </div> <div>self.attributes->forAll(a1, a2 | a1 <> a2 implies a1.name <> a2.name)</div> <p> </p>
Model Checking of Spacecraft Operational Designs: A Scalability Analysis - Artifact
<p>This artifact contains the accompanying experiment data for the publication "Model Checking of Spacecraft Operational Designs: A Scalability Analysis".</p>
A habitat connectivity reality check for fish physical habitat model results and decision making for river restoration
<ol> <li>Fish physical habitat models are a tool for guiding restoration efforts in lotic ecosystems but often they overestimate restoration outcomes because currently they do not incorporate habitat connectivity. This persistent issue can, in extreme cases, result in little or no improvement to fish populations after the restoration, wasting valuable conservation resources.</li> <li>We present a case study where practitioners applied a fish habitat model for multiple life history stages of gravel spawning fishes to a 52 kilometer stretch of the Iller River but did so at a microscale implementation (every 200 meters). This approach provided an opportunity to assess the connectivity of gravel spawning fishes to find suitable habitats for all life history stages and seasonal movements.</li> <li>We used the assessed habitat estimates (availability of distinct habitat types within the 200 m reaches) to calculate the minimum distance a fish would need to go as it hypothetically “grew up” from egg to full spawning adult. We call this technique a reality check as it results in a decisive understanding of which areas were ultimately necessary to fulfill the life cycle of gravel spawning fishes, which standard assessments do not show.</li> <li>Our results show that complete connectivity still require long movement distances for vulnerable life stages to find suitable habitat. This contradicts standard practice, as restoration schemes and decision making often assume that connectivity inherently leads to more fish production without added habitat restoration.</li> <li>We recommend practitioners should perform this habitat connectivity approach when assessments implement fish habitat suitability models at similar scales. As a result, decision makers can evaluate proposed restoration sites and measures more realistically.</li> </ol>
Applicability of Model Checking for Verifying Spacecraft Operational Designs - Artifact
<p>This artifact contains the accompanying experiment data for the submission "Applicability of Model Checking for Verifying Spacecraft Operational Designs".</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>
Code-Level Model Checking in the Software Development Workflow -- Replication Package
<p>This experience report describes a style of applying symbolic model checking developed over the course of four years at Amazon Web Services (AWS). Lessons learned are drawn from proving properties of numerous C-based systems, e.g., custom hypervisors, encryption code, boot loaders, and an IoT operating system. Using our methodology, we find that we can prove the correctness of industrial low-level C-based systems with reasonable effort and predictability. Furthermore, AWS developers are increasingly writing their own formal specifications. All proofs discussed in this paper are publicly available on GitHub. All proofs and specifications described in the paper are available, under the Apache 2.0 license, on the GitHub repository located at <a href="https://github.com/awslabs/aws-c-common/">https://github.com/awslabs/aws-c-common/</a> This is the master repository for AWS C Common library, and is in active use by the AWS C Common development team. The description of the contents of this repository are based off commit <code>b0ea9f35df8934f9e03fc3bab3919d55efd69b88</code>, although they are not expected to change significantly in the future.</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>
Artifact of Infrastructure and Tools in the Context of Deep Statistical Model Checking
<p>This artifact contains all infrastructure, tools, and additional material used in the context of Deep Statistical Model Checking (DSMC). This includes the DSMC implementation in modes of the Modest Toolset, the infrastructure used to perform case studies on DSMC, the environment and scripts in which the scalability study on DSMC has been performed, the integration of DSMC in MoGym, and also the TraceVis tool. The content has partially been covered in artifacts accompanying individual papers on DSMC, but is combined here based on a single infrastructure. Each folder contains its own readme describing how to use the scripts, tools, and infrastructure, often also with concrete instructions on how to execute exemplary experiments.</p>
Exploring Hierarchy and Dependency of Rules for Consistency Checking Between Code and Model (Evaluation Data)
<p>This repository contains the data related to the protocol and results of the evaluation conducted on the HiDeoCR approach. </p>
Artifact for the Scalability Study of the STTT Paper "Analyzing Neural Network Behavior through Deep Statistical Model Checking"
<p>Scripts and infrastructure for the scalability study on DSMC published in the STTT paper "Analyzing Neural Network Behavior through Deep Statistical Model Checking".</p>
Truth Tables for consistency-checking 3D geological models
<p>The Microsoft Excel and PDF representations of the Truth Tables and geo-feature relation exampels are provided as supplementary information to the GMD publication: </p> <p><strong>Consistency-Checking 3D Geological Models</strong></p> <p><strong>Marion N. Parquer, Eric A. de Kemp, Boyan Brodaric and Michael J. Hillier</strong></p> <p> </p>
[Replication package] Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning
<p>Anonymized replication package of submission #1917: "Explainable Human-Machine Teaming using Model Checking and Interpretable Machine Learning".</p> <p>See README.md for further instructions.</p>
Formal properties collected from practical model-checking projects
<p>Since 2008, VTT has been applying model checking in practical customer projects in the Finnish nuclear and railway industries. We have collected 3923 formal properties specified and verified by VTT analysts in the those projects between the years 2014 and 2022. To mask confidential data, we have removed the references to the original model variables, and only preserved the temporal structure of each property.</p> <p>Please cite:</p> <p><span>Pakonen A.</span>, Buzhinsky, I., Vyatkin, V. <strong>Evaluation of visual property specification languages based on practical model-checking experience</strong>.<br>Journal of Systems and Software, vol. 216, October 2024, 112153. https://doi.org/10.1016/j.jss.2024.112153</p>
Supplementary Material for the paper "Efficient Strategies for CEGAR-based Model Checking"
<p>Supplementary material for the paper "Efficient Strategies for CEGAR-based Model Checking" by Akos Hajdu and Zoltan Micskei. The material includes a detailed report (report.html) and all artifacts to replicate our measurements and analysis (artifact.tar.gz).</p> <p><em>Version 1.2.0 corresponds to the final, published paper. This version (1.2.1) is a minor update that added two new plots.</em></p>
Model Checking the Multi-Formalism Language FIGARO
<p>for double blind review</p>
Towards Compliance Checking between Business Process Models and Lawful States of Objects
<p>Dataset from publication http://ceur-ws.org/Vol-1230/paper-03.pdf </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.