Runtime Verification on Abstract Finite State Models

• URL: http://arxiv.org/abs/2406.12715v1
• Date: Tue, 18 Jun 2024 15:32:31 GMT
• Title: Runtime Verification on Abstract Finite State Models
• Authors: KP Jevitha, Bharat Jayaraman, M Sethumadhavan,
• Abstract summary: We show how to extract finite state models from a run of a multi-threaded Java program and carry out runtime verification of correctness properties. The main contribution of this paper is in showing how runtime verification can be made efficient through online property checking on property-preserving abstract models.
• Score: 0.0
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: Finite-state models are ubiquitous in the study of concurrent systems, especially controllers and servers that operate in a repetitive cycle. In this paper, we show how to extract finite state models from a run of a multi-threaded Java program and carry out runtime verification of correctness properties. These properties include data-oriented and control-oriented properties; the former express correctness conditions over the data fields of objects, while the latter are concerned with the correct flow of control among the modules of larger software. As the extracted models can become very large for long runs, the focus of this paper is on constructing reduced models with user-defined abstraction functions that map a larger domain space to a smaller one. The abstraction functions should be chosen so that the resulting model is property preserving, i.e., proving a property on the abstract model carries over to the concrete model. The main contribution of this paper is in showing how runtime verification can be made efficient through online property checking on property-preserving abstract models. The property specification language resembles a propositional linear temporal logic augmented with simple datatypes and operators. Classic concurrency examples and larger case studies (Multi-rotor Drone Controller, OAuth Protocol) are presented in order to demonstrate the usefulness of our proposed techniques, which are incorporated in an Eclipse plug-in for runtime visualization and verification of Java programs.

Related papers

• EmbedLLM: Learning Compact Representations of Large Language Models [28.49433308281983]
  We propose EmbedLLM, a framework designed to learn compact vector representations of Large Language Models. We introduce an encoder-decoder approach for learning such embeddings, along with a systematic framework to evaluate their effectiveness. Empirical results show that EmbedLLM outperforms prior methods in model routing both in accuracy and latency.
  arXiv  Detail & Related papers  (2024-10-03T05:43:24Z)
• Fine-Tuning Enhances Existing Mechanisms: A Case Study on Entity Tracking [53.66999416757543]
  We study how fine-tuning affects the internal mechanisms implemented in language models. Fine-tuning enhances, rather than alters, the mechanistic operation of the model.
  arXiv  Detail & Related papers  (2024-02-22T18:59:24Z)
• Formal Verification Of A Shopping Basket Application Model Using PRISM [0.0]
  We present the results of a simulation using Prism Model Checker for a Shopping Basket Application Model. The objective is to simulate the behavior of shoppers as they go through a number of defined states of the shopping process.
  arXiv  Detail & Related papers  (2023-07-16T00:14:40Z)
• DORE: Document Ordered Relation Extraction based on Generative Framework [56.537386636819626]
  This paper investigates the root cause of the underwhelming performance of the existing generative DocRE models. We propose to generate a symbolic and ordered sequence from the relation matrix which is deterministic and easier for model to learn. Experimental results on four datasets show that our proposed method can improve the performance of the generative DocRE models.
  arXiv  Detail & Related papers  (2022-10-28T11:18:10Z)
• Segmenting Moving Objects via an Object-Centric Layered Representation [100.26138772664811]
  We introduce an object-centric segmentation model with a depth-ordered layer representation. We introduce a scalable pipeline for generating synthetic training data with multiple objects. We evaluate the model on standard video segmentation benchmarks.
  arXiv  Detail & Related papers  (2022-07-05T17:59:43Z)
• SAT-Based Extraction of Behavioural Models for Java Libraries with Collections [0.087024326813104]
  Behavioural models are a valuable tool for software verification, testing, monitoring, publishing etc. They are rarely provided by the software developers and have to be extracted either from the source or from the compiled code. Most of these approaches rely on the analysis of the compiled bytecode. We are looking to extract behavioural models in the form of Finite State Machines (FSMs) from the Java source code to ensure that the obtained FSMs can be easily understood by the software developers.
  arXiv  Detail & Related papers  (2022-05-30T17:27:13Z)
• Visualising Deep Network's Time-Series Representations [93.73198973454944]
  Despite the popularisation of machine learning models, more often than not they still operate as black boxes with no insight into what is happening inside the model. In this paper, a method that addresses that issue is proposed, with a focus on visualising multi-dimensional time-series data. Experiments on a high-frequency stock market dataset show that the method provides fast and discernible visualisations.
  arXiv  Detail & Related papers  (2021-03-12T09:53:34Z)
• Model-Invariant State Abstractions for Model-Based Reinforcement Learning [54.616645151708994]
  We introduce a new type of state abstraction called textitmodel-invariance. This allows for generalization to novel combinations of unseen values of state variables. We prove that an optimal policy can be learned over this model-invariance state abstraction.
  arXiv  Detail & Related papers  (2021-02-19T10:37:54Z)
• Interpretable Entity Representations through Large-Scale Typing [61.4277527871572]
  We present an approach to creating entity representations that are human readable and achieve high performance out of the box. Our representations are vectors whose values correspond to posterior probabilities over fine-grained entity types. We show that it is possible to reduce the size of our type set in a learning-based way for particular domains.
  arXiv  Detail & Related papers  (2020-04-30T23:58:03Z)

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.