Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing

• URL: http://arxiv.org/abs/2501.12932v1
• Date: Wed, 22 Jan 2025 15:03:25 GMT
• Title: Formal Analysis of the Contract Automata Runtime Environment with Uppaal: Modelling, Verification and Testing
• Authors: Davide Basile,
• Abstract summary: A distributed runtime application called tt CARE has been introduced to realise service applications specified using a dialect of finite-state automata. We detail the formal modelling, verification and testing of tt CARE.
• Score: 0.3807314298073301
• License:
• Abstract: Recently, a distributed middleware application called contract automata runtime environment ({\tt CARE}) has been introduced to realise service applications specified using a dialect of finite-state automata. In this paper, we detail the formal modelling, verification and testing of {\tt CARE}. We provide a formalisation as a network of stochastic timed automata. The model is verified against the desired properties with the tool {\sc Uppaal}, utilising exhaustive and statistical model checking techniques. Abstract tests are generated from the {\sc Uppaal} models that are concretised for testing {\tt CARE}. This research emphasises the advantages of employing formal modelling, verification and testing processes to enhance the dependability of an open-source distributed application. We discuss the methodology used for modelling the application and generating concrete tests from the abstract model, addressing the issues that have been identified and fixed.

Related papers

• Neural Model Checking [10.376573742987917]
  We introduce a machine learning approach to model checking temporal logic, with application to formal hardware verification. Our new approach combines machine learning and symbolic reasoning by using neural networks as formal proof certificates for linear temporal logic. We experimentally demonstrate that our method outperforms the state-of-the-art academic and commercial model checkers on a set of standard hardware designs written in SystemVerilog.
  arXiv  Detail & Related papers  (2024-10-31T10:17:04Z)
• Model Equality Testing: Which Model Is This API Serving? [59.005869726179455]
  We formalize detecting such distortions as Model Equality Testing, a two-sample testing problem. A test built on a simple string kernel achieves a median of 77.4% power against a range of distortions. We then apply this test to commercial inference APIs for four Llama models, finding that 11 out of 31 endpoints serve different distributions than reference weights released by Meta.
  arXiv  Detail & Related papers  (2024-10-26T18:34:53Z)
• Automatic Generation of Behavioral Test Cases For Natural Language Processing Using Clustering and Prompting [6.938766764201549]
  This paper introduces an automated approach to develop test cases by exploiting the power of large language models and statistical techniques. We analyze the behavioral test profiles across four different classification algorithms and discuss the limitations and strengths of those models.
  arXiv  Detail & Related papers  (2024-07-31T21:12:21Z)
• Type-level Property Based Testing [0.0]
  We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. We are able to model several interesting systems and network protocols, have the type checker verify that our implementation behaves as specified, and test that our model matches the specification's semantics.
  arXiv  Detail & Related papers  (2024-07-17T16:43:41Z)
• Representing Timed Automata and Timing Anomalies of Cyber-Physical Production Systems in Knowledge Graphs [51.98400002538092]
  This paper aims to improve model-based anomaly detection in CPPS by combining the learned timed automaton with a formal knowledge graph about the system. Both the model and the detected anomalies are described in the knowledge graph in order to allow operators an easier interpretation of the model and the detected anomalies.
  arXiv  Detail & Related papers  (2023-08-25T15:25:57Z)
• 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)
• Exploring validation metrics for offline model-based optimisation with diffusion models [50.404829846182764]
  In model-based optimisation (MBO) we are interested in using machine learning to design candidates that maximise some measure of reward with respect to a black box function called the (ground truth) oracle. While an approximation to the ground oracle can be trained and used in place of it during model validation to measure the mean reward over generated candidates, the evaluation is approximate and vulnerable to adversarial examples. This is encapsulated under our proposed evaluation framework which is also designed to measure extrapolation.
  arXiv  Detail & Related papers  (2022-11-19T16:57:37Z)
• Model ensemble instead of prompt fusion: a sample-specific knowledge transfer method for few-shot prompt tuning [85.55727213502402]
  We focus on improving the few-shot performance of prompt tuning by transferring knowledge from soft prompts of source tasks. We propose Sample-specific Ensemble of Source Models (SESoM) SESoM learns to adjust the contribution of each source model for each target sample separately when ensembling source model outputs.
  arXiv  Detail & Related papers  (2022-10-23T01:33:16Z)
• Generalization Properties of Retrieval-based Models [50.35325326050263]
  Retrieval-based machine learning methods have enjoyed success on a wide range of problems. Despite growing literature showcasing the promise of these models, the theoretical underpinning for such models remains underexplored. We present a formal treatment of retrieval-based models to characterize their generalization ability.
  arXiv  Detail & Related papers  (2022-10-06T00:33:01Z)
• Learning to Generalize across Domains on Single Test Samples [126.9447368941314]
  We learn to generalize across domains on single test samples. We formulate the adaptation to the single test sample as a variational Bayesian inference problem. Our model achieves at least comparable -- and often better -- performance than state-of-the-art methods on multiple benchmarks for domain generalization.
  arXiv  Detail & Related papers  (2022-02-16T13:21:04Z)
• Automated simulation and verification of process models discovered by process mining [0.0]
  This paper presents a novel approach for automated analysis of process models discovered using process mining techniques. Process mining explores underlying processes hidden in the event data generated by various devices.
  arXiv  Detail & Related papers  (2020-11-03T11:51: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.