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

• On the Reasoning Capacity of AI Models and How to Quantify It [0.0]
  Large Language Models (LLMs) have intensified the debate surrounding the fundamental nature of their reasoning capabilities. While achieving high performance on benchmarks such as GPQA and MMLU, these models exhibit limitations in more complex reasoning tasks. We propose a novel phenomenological approach that goes beyond traditional accuracy metrics to probe the underlying mechanisms of model behavior.
  arXiv  Detail & Related papers  (2025-01-23T16:58:18Z)
• Can foundation models actively gather information in interactive environments to test hypotheses? [56.651636971591536]
  We introduce a framework in which a model must determine the factors influencing a hidden reward function. We investigate whether approaches such as self- throughput and increased inference time improve information gathering efficiency.
  arXiv  Detail & Related papers  (2024-12-09T12:27:21Z)
• 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)
• 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.