Automated SysML-Based Verification of Discipline-Specific Models

• URL: http://arxiv.org/abs/2606.29006v1
• Date: Sat, 27 Jun 2026 16:56:22 GMT
• Title: Automated SysML-Based Verification of Discipline-Specific Models
• Abstract summary: This project addresses the problem with a verification process tailored to model-based verification.<n>A mixed-method approach combining literature research and stakeholder interviews was used to derive validated stakeholder needs.<n>The process was demonstrated end-to-end in two independent SysML tool-chains to evidence tool-agnosticism.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Current examples of SysML-based verification of discipline-specific models in the literature typically have two flaws. Firstly, they are developed in a tool-specific manner using proprietary APIs, limiting portability. Secondly, they focus on performance properties modelled via parametric diagrams, overlooking behavioural and interface properties that also require verification. This project addresses the problem with a verification process tailored to model-based verification, informed by common SysML tool capabilities and the UML Testing Profile, that enables automated verification of discipline\-/specific models from SysML test cases and returns the results to the SysML model for traceability. A mixed-method approach combining literature research and stakeholder interviews was used to derive validated stakeholder needs, which drove the specification and design of the process. The process was demonstrated end-to-end in two independent SysML tool-chains to evidence tool-agnosticism, and was shown to verify behavioural and interface requirements, including ordering, timing, and state-based responses, using SysML behavioural diagram constructs that parametric approaches alone cannot address.

Related papers

• Formal Verification of Agentic Systems over Operational Data [59.98246281888422]
  Agentic systems driven by large language models (LLMs) are increasingly deployed in real-world where they act on persistent operational data.<n>Existing approaches do not provide such system-level guarantees.<n>We study here the verification of agentic systems comprising a single LLM and a tool orchestration harness over relational operational data.
  arXiv  Detail & Related papers  (2026-08-04T13:01:30Z)
• Model-Driven Discipline for Multi-Agent LLMs: Requirement-to-Verification Generation of Traceable System Models [62.62160094849002]
  RADIANT is an engineering methodology that combines MDE with Multi-Agent Large Language Models.<n>It automatically generates heterogeneous models across engineering phases.<n>It provides exact, automated change-impact analysis.
  arXiv  Detail & Related papers  (2026-07-18T08:50:55Z)
• LiveFMBench: Unveiling the Power and Limits of Agentic Workflows in Specification Generation [75.05397479715576]
  Large language models (LLMs) and agents have shown promising progress, but their true capabilities and failure modes remain unclear.<n>We present the first systematic and contamination-aware study of LLM- and agent-based formal specification generation for C programs.
  arXiv  Detail & Related papers  (2026-05-02T11:31:33Z)
• Bridging Natural Language and Interactive What-If Interfaces via LLM-Generated Declarative Specification [7.203839699772057]
  We present a two-stage workflow that translates natural language (NL) WIA questions into interactive visual interfaces via an intermediate representation.<n>We benchmark this workflow with 405 WIA questions spanning 11 WIA types, 5 datasets, and 3 state-of-the-art LLMs.<n>The results show that across models, half of specifications (52.42%) are generated correctly without intervention.
  arXiv  Detail & Related papers  (2026-04-08T23:35:33Z)
• PAT-Agent: Autoformalization for Model Checking [17.082027022913998]
  PAT-Agent is an end-to-end framework for natural language autoformalization and formal model repair.<n>It combines the generative capabilities of large language models with the rigor of formal verification.
  arXiv  Detail & Related papers  (2025-09-28T06:32:14Z)
• CompassVerifier: A Unified and Robust Verifier for LLMs Evaluation and Outcome Reward [50.97588334916863]
  We develop CompassVerifier, an accurate and robust lightweight verifier model for evaluation and outcome reward.<n>It demonstrates multi-domain competency spanning math, knowledge, and diverse reasoning tasks, with the capability to process various answer types.<n>We introduce VerifierBench benchmark comprising model outputs collected from multiple data sources, augmented through manual analysis of metaerror patterns to enhance CompassVerifier.
  arXiv  Detail & Related papers  (2025-08-05T17:55:24Z)
• Instance-Level Data-Use Auditing of Visual ML Models [49.862257986549885]
  Growing trend of legal disputes over the unauthorized use of data in machine learning (ML) systems highlights the need for reliable data-use auditing mechanisms.<n>We present the first proactive, instance-level, data-use auditing method designed to enable data owners to audit the use of their individual data instances in ML models.
  arXiv  Detail & Related papers  (2025-03-28T13:28:57Z)
• Inference-Time Intervention in Large Language Models for Reliable Requirement Verification [2.3759432635713895]
  Inference-time intervention techniques provide a promising alternative to fine-tuning.<n>We demonstrate how interventions enable fine-grained control for automating the usually time-intensive requirement verification process.<n>Our method achieves robust and reliable outputs, significantly improving over both a baseline model and a fine-tuning approach.
  arXiv  Detail & Related papers  (2025-03-18T10:49:36Z)
• Matchmaker: Self-Improving Large Language Model Programs for Schema Matching [60.23571456538149]
  We propose a compositional language model program for schema matching, comprised of candidate generation, refinement and confidence scoring. Matchmaker self-improves in a zero-shot manner without the need for labeled demonstrations. Empirically, we demonstrate on real-world medical schema matching benchmarks that Matchmaker outperforms previous ML-based approaches.
  arXiv  Detail & Related papers  (2024-10-31T16:34:03Z)
• Using Quality Attribute Scenarios for ML Model Test Case Generation [3.9111051646728527]
  Current practice for machine learning (ML) model testing prioritizes testing for model performance. This paper presents an approach based on quality attribute (QA) scenarios to elicit and define system- and model-relevant test cases. The QA-based approach has been integrated into MLTE, a process and tool to support ML model test and evaluation.
  arXiv  Detail & Related papers  (2024-06-12T18:26:42Z)
• 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)
• ReEval: Automatic Hallucination Evaluation for Retrieval-Augmented Large Language Models via Transferable Adversarial Attacks [91.55895047448249]
  This paper presents ReEval, an LLM-based framework using prompt chaining to perturb the original evidence for generating new test cases. We implement ReEval using ChatGPT and evaluate the resulting variants of two popular open-domain QA datasets. Our generated data is human-readable and useful to trigger hallucination in large language models.
  arXiv  Detail & Related papers  (2023-10-19T06:37:32Z)
• DeforestVis: Behavior Analysis of Machine Learning Models with Surrogate Decision Stumps [46.58231605323107]
  We propose DeforestVis, a visual analytics tool that offers summarization of the behaviour of complex ML models. DeforestVis helps users to explore the complexity versus fidelity trade-off by incrementally generating more stumps. We show the applicability and usefulness of DeforestVis with two use cases and expert interviews with data analysts and model developers.
  arXiv  Detail & Related papers  (2023-03-31T21:17:15Z)

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.