Formalizing UML State Machines for Automated Verification -- A Survey

• URL: http://arxiv.org/abs/2407.17215v1
• Date: Wed, 24 Jul 2024 12:15:31 GMT
• Title: Formalizing UML State Machines for Automated Verification -- A Survey
• Authors: Étienne André, Shuang Liu, Yang Liu, Christine Choppy, Jun Sun, Jin Song Dong,
• Abstract summary: The Modeling Language (UML) is a standard for modeling dynamic systems. The specification, maintained by the Object Management Group (OMG), is documented in natural language.
• Score: 14.99225452541953
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: The Unified Modeling Language (UML) is a standard for modeling dynamic systems. UML behavioral state machines are used for modeling the dynamic behavior of object-oriented designs. The UML specification, maintained by the Object Management Group (OMG), is documented in natural language (in contrast to formal language). The inherent ambiguity of natural languages may introduce inconsistencies in the resulting state machine model. Formalizing UML state machine specification aims at solving the ambiguity problem and at providing a uniform view to software designers and developers. Such a formalization also aims at providing a foundation for automatic verification of UML state machine models, which can help to find software design vulnerabilities at an early stage and reduce the development cost. We provide here a comprehensive survey of existing work from 1997 to 2021 related to formalizing UML state machine semantics for the purpose of conducting model checking at the design stage.

Related papers

• Towards Synthetic Trace Generation of Modeling Operations using In-Context Learning Approach [1.8874331450711404]
  We propose a conceptual framework that combines modeling event logs, intelligent modeling assistants, and the generation of modeling operations. In particular, the architecture comprises modeling components that help the designer specify the system, record its operation within a graphical modeling environment, and automatically recommend relevant operations.
  arXiv  Detail & Related papers  (2024-08-26T13:26:44Z)
• 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)
• Synergy of Large Language Model and Model Driven Engineering for Automated Development of Centralized Vehicular Systems [2.887732304499794]
  We present a prototype of a tool leveraging the synergy of model driven engineering (MDE) and Large Language Models (LLM) The generated code is evaluated in a simulated environment using CARLA simulator connected to an example centralized vehicle architecture, in an emergency brake scenario.
  arXiv  Detail & Related papers  (2024-04-08T13:28:11Z)
• CLOMO: Counterfactual Logical Modification with Large Language Models [109.60793869938534]
  We introduce a novel task, Counterfactual Logical Modification (CLOMO), and a high-quality human-annotated benchmark. In this task, LLMs must adeptly alter a given argumentative text to uphold a predetermined logical relationship. We propose an innovative evaluation metric, the Self-Evaluation Score (SES), to directly evaluate the natural language output of LLMs.
  arXiv  Detail & Related papers  (2023-11-29T08:29:54Z)
• L2CEval: Evaluating Language-to-Code Generation Capabilities of Large Language Models [102.00201523306986]
  We present L2CEval, a systematic evaluation of the language-to-code generation capabilities of large language models (LLMs) We analyze the factors that potentially affect their performance, such as model size, pretraining data, instruction tuning, and different prompting methods. In addition to assessing model performance, we measure confidence calibration for the models and conduct human evaluations of the output programs.
  arXiv  Detail & Related papers  (2023-09-29T17:57:00Z)
• To Do or Not to Do: Semantics and Patterns for Do Activities in UML PSSM State Machines [0.11470070927586014]
  DoActivity behaviors describe behavior that is executed independently from the state machine once entered in a given state. The specification or textbooks are vague about how the doActivity behavior construct should be appropriately used. We analyzed the semantics by collecting evidence from cross-checking the text of the specification, its semantic model and executable test cases, and the simulators supporting PSSM.
  arXiv  Detail & Related papers  (2023-09-26T12:30:51Z)
• Explainability for Large Language Models: A Survey [59.67574757137078]
  Large language models (LLMs) have demonstrated impressive capabilities in natural language processing. This paper introduces a taxonomy of explainability techniques and provides a structured overview of methods for explaining Transformer-based language models.
  arXiv  Detail & Related papers  (2023-09-02T22:14:26Z)
• Augmented Language Models: a Survey [55.965967655575454]
  This survey reviews works in which language models (LMs) are augmented with reasoning skills and the ability to use tools. We refer to them as Augmented Language Models (ALMs) The missing token objective allows ALMs to learn to reason, use tools, and even act, while still performing standard natural language tasks.
  arXiv  Detail & Related papers  (2023-02-15T18:25:52Z)
• Language Modeling with Latent Situations [46.38670628102201]
  SituationSupervision is a family of approaches for improving coherence in language models. It trains models to construct and condition on explicit representations of entities and their states. It produces major coherence improvements between 4-11%.
  arXiv  Detail & Related papers  (2022-12-20T05:59:42Z)
• Consistency of UML class, object and statechart diagrams using ontology reasoners [0.0]
  We propose an automatic approach to analyze consistency and satisfiability of Unified Modeling Language models containing multiple class, object and statechart diagrams. We describe how to translate models in OWL 2 and we present a tool chain implementing this translation that can be used with any standard compliant modeling tool.
  arXiv  Detail & Related papers  (2022-05-23T10:29:32Z)
• Semantic based model of Conceptual Work Products for formal verification of complex interactive systems [3.0458872052651973]
  We describe an automatic logic reasoner to verify objective specifications for conceptual work products. The conceptual work products specifications serve as a fundamental output requirement, which must be clearly stated, correct and solvable. Our Work Ontology with tools from Semantic Web is needed to translate class and state diagrams for verification of solvability with automatic reasoning.
  arXiv  Detail & Related papers  (2020-08-04T15:10:44Z)

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.