A Verification Framework for Component-Based Modeling and Simulation
Putting the pieces together
- URL: http://arxiv.org/abs/2301.03088v1
- Date: Sun, 8 Jan 2023 18:53:28 GMT
- Title: A Verification Framework for Component-Based Modeling and Simulation
Putting the pieces together
- Authors: Imran Mahmood
- Abstract summary: The proposed verification framework provides methods, techniques and tool support for verifying composability at its different levels.
In particular we focus on the Dynamic-Semantic Composability level due to its significance in the overall composability correctness and also due to the level of difficulty it poses in the process.
- Score: 0.0
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: In this thesis a comprehensive verification framework is proposed to contend
with some important issues in composability verification and a verification
process is suggested to verify composability of different kinds of systems
models, such as reactive, real-time and probabilistic systems. With an
assumption that all these systems are concurrent in nature in which different
composed components interact with each other simultaneously, the requirements
for the extensive techniques for the structural and behavioral analysis becomes
increasingly challenging. The proposed verification framework provides methods,
techniques and tool support for verifying composability at its different
levels. These levels are defined as foundations of consistent model
composability. Each level is discussed in detail and an approach is presented
to verify composability at that level. In particular we focus on the
Dynamic-Semantic Composability level due to its significance in the overall
composability correctness and also due to the level of difficulty it poses in
the process. In order to verify composability at this level we investigate the
application of three different approaches namely (i) Petri Nets based Algebraic
Analysis (ii) Colored Petri Nets (CPN) based State-space Analysis and (iii)
Communicating Sequential Processes based Model Checking. All three approaches
attack the problem of verifying dynamic-semantic composability in different
ways however they all share the same aim i.e., to confirm the correctness of a
composed model with respect to its requirement specifications.
Related papers
- SMLE: Safe Machine Learning via Embedded Overapproximation [4.129133569151574]
We consider the task of training differentiable ML models guaranteed to satisfy designer-chosen properties.
This is very challenging, due to the computational complexity of rigorously verifying and enforcing compliance in modern neural models.
We provide an innovative approach based on three components: 1) a general, simple architecture enabling efficient verification with a conservative semantic.
We evaluate our approach on properties defined by linear inequalities in regression, and on mutually exclusive classes in multilabel classification.
arXiv Detail & Related papers (2024-09-30T17:19:57Z) - MARS: Benchmarking the Metaphysical Reasoning Abilities of Language Models with a Multi-task Evaluation Dataset [50.36095192314595]
Large Language Models (LLMs) function as conscious agents with generalizable reasoning capabilities.
This ability remains underexplored due to the complexity of modeling infinite possible changes in an event.
We introduce the first-ever benchmark, MARS, comprising three tasks corresponding to each step.
arXiv Detail & Related papers (2024-06-04T08:35:04Z) - OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in
Aspect-Oriented Applications [0.0]
observe-based statistical model-checking (OSM) framework devised to craft executable formal models directly from foundational system code.
This ensures the unyielding performance of electronic health record systems amidst shifting preconditions.
arXiv Detail & Related papers (2024-03-03T00:03:34Z) - Object-Centric Conformance Alignments with Synchronization (Extended Version) [57.76661079749309]
We present a new formalism that combines the ability of object-centric Petri nets to capture one-to-many relations and the one of Petri nets with identifiers to compare and synchronize objects based on their identity.
We propose a conformance checking approach for such nets based on an encoding in satisfiability modulo theories (SMT)
arXiv Detail & Related papers (2023-12-13T21:53:32Z) - Variable Importance Matching for Causal Inference [73.25504313552516]
We describe a general framework called Model-to-Match that achieves these goals.
Model-to-Match uses variable importance measurements to construct a distance metric.
We operationalize the Model-to-Match framework with LASSO.
arXiv Detail & Related papers (2023-02-23T00:43:03Z) - Universal Information Extraction as Unified Semantic Matching [54.19974454019611]
We decouple information extraction into two abilities, structuring and conceptualizing, which are shared by different tasks and schemas.
Based on this paradigm, we propose to universally model various IE tasks with Unified Semantic Matching framework.
In this way, USM can jointly encode schema and input text, uniformly extract substructures in parallel, and controllably decode target structures on demand.
arXiv Detail & Related papers (2023-01-09T11:51:31Z) - Relational Action Bases: Formalization, Effective Safety Verification,
and Invariants (Extended Version) [67.99023219822564]
We introduce the general framework of relational action bases (RABs)
RABs generalize existing models by lifting both restrictions.
We demonstrate the effectiveness of this approach on a benchmark of data-aware business processes.
arXiv Detail & Related papers (2022-08-12T17:03:50Z) - Exploring the Trade-off between Plausibility, Change Intensity and
Adversarial Power in Counterfactual Explanations using Multi-objective
Optimization [73.89239820192894]
We argue that automated counterfactual generation should regard several aspects of the produced adversarial instances.
We present a novel framework for the generation of counterfactual examples.
arXiv Detail & Related papers (2022-05-20T15:02:53Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.