OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in Aspect-Oriented Applications

• URL: http://arxiv.org/abs/2403.01349v1
• Date: Sun, 3 Mar 2024 00:03:34 GMT
• Title: OSM: Leveraging Model Checking for Observing Dynamic 1 behaviors in Aspect-Oriented Applications
• Authors: Anas AlSobeh
• Abstract summary: 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.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In the intricate domain of software systems verification, dynamically model checking multifaceted system characteristics remains paramount, yet challenging. This research proposes the advanced observe-based statistical model-checking (OSM) framework, devised to craft executable formal models directly from foundational system code. Leveraging model checking predicates, the framework melds seamlessly with aspect-oriented programming paradigms, yielding a potent method for the analytical verification of varied behavioral attributes. Exploiting the transformative capacity of OSM framework, primary system code undergoes a systematic metamorphosis into multifaceted analysis constructs. This not only simplifies the model verification process but also orchestrates feature interactions using an innovative observing join point abstraction mechanism. Within this framework, components encompassing parsing, formal verification, computational analytics, and rigorous validation are intrinsically interwoven. Marrying the principles of model checking with aspect-oriented (AO) modularization, OSM framework stands as a paragon, proficiently scrutinizing and affirming system specifications. This ensures the unyielding performance of electronic health record systems amidst shifting preconditions. OSM framework offers runtime verification of both object-oriented and AO deployments, positioning itself as an indispensable open-source resource, poised to automate the enhancement of system performance and scalability.

Related papers

• Enhanced Transformer architecture for in-context learning of dynamical systems [0.3749861135832073]
  In this paper, we enhance the original meta-modeling framework through three key innovations. The efficacy of these modifications is demonstrated through a numerical example focusing on the Wiener-Hammerstein system class.
  arXiv  Detail & Related papers  (2024-10-04T10:05:15Z)
• A process algebraic framework for multi-agent dynamic epistemic systems [55.2480439325792]
  We propose a unifying framework for modeling and analyzing multi-agent, knowledge-based, dynamic systems. On the modeling side, we propose a process algebraic, agent-oriented specification language that makes such a framework easy to use for practical purposes.
  arXiv  Detail & Related papers  (2024-07-24T08:35:50Z)
• Benchmarks as Microscopes: A Call for Model Metrology [76.64402390208576]
  Modern language models (LMs) pose a new challenge in capability assessment. To be confident in our metrics, we need a new discipline of model metrology.
  arXiv  Detail & Related papers  (2024-07-22T17:52:12Z)
• Process Modeling With Large Language Models [42.0652924091318]
  This paper explores the integration of Large Language Models (LLMs) into process modeling. We propose a framework that leverages LLMs for the automated generation and iterative refinement of process models. Preliminary results demonstrate the framework's ability to streamline process modeling tasks.
  arXiv  Detail & Related papers  (2024-03-12T11:27:47Z)
• Probabilistic ML Verification via Weighted Model Integration [11.812078181471634]
  Probability formal verification (PFV) of machine learning models is in its infancy. We propose a unifying framework for the PFV of ML systems based on Weighted Model Integration (WMI) We show how successful scaling techniques in the ML verification literature can be generalized beyond their original scope.
  arXiv  Detail & Related papers  (2024-02-07T14:24:04Z)
• White-box validation of quantitative product lines by statistical model checking and process mining [1.0918484507642576]
  We propose a novel methodology for validating software product line (PL) models by integrating Statistical Model Checking (SMC) with Process Mining (PM) Our approach focuses on the feature-oriented language QFLan in the PL engineering domain, allowing modeling of PLs with rich cross-tree and quantitative constraints.
  arXiv  Detail & Related papers  (2024-01-23T17:27:13Z)
• When to Update Your Model: Constrained Model-based Reinforcement Learning [50.74369835934703]
  We propose a novel and general theoretical scheme for a non-decreasing performance guarantee of model-based RL (MBRL) Our follow-up derived bounds reveal the relationship between model shifts and performance improvement. A further example demonstrates that learning models from a dynamically-varying number of explorations benefit the eventual returns.
  arXiv  Detail & Related papers  (2022-10-15T17:57:43Z)
• 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)
• Extending Process Discovery with Model Complexity Optimization and Cyclic States Identification: Application to Healthcare Processes [62.997667081978825]
  The paper presents an approach to process mining providing semi-automatic support to model optimization. A model simplification approach is proposed, which essentially abstracts the raw model at the desired granularity. We aim to demonstrate the capabilities of the technological solution using three datasets from different applications in the healthcare domain.
  arXiv  Detail & Related papers  (2022-06-10T16:20:59Z)
• Lifted Model Checking for Relational MDPs [12.574454799055026]
  pCTL-REBEL is a lifted model checking approach for verifying pCTL properties on relational MDPs. We show that the pCTL model checking approach is decidable for relational MDPs even for possibly infinite domains.
  arXiv  Detail & Related papers  (2021-06-22T13:12:36Z)
• S2RMs: Spatially Structured Recurrent Modules [105.0377129434636]
  We take a step towards exploiting dynamic structure that are capable of simultaneously exploiting both modular andtemporal structures. We find our models to be robust to the number of available views and better capable of generalization to novel tasks without additional training.
  arXiv  Detail & Related papers  (2020-07-13T17:44:30Z)

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.