Spreadsheet-based Configuration of Families of Real-Time Specifications

• URL: http://arxiv.org/abs/2310.20395v1
• Date: Tue, 31 Oct 2023 12:16:56 GMT
• Title: Spreadsheet-based Configuration of Families of Real-Time Specifications
• Authors: Jos\'e Proen\c{c}a (CISTER and University of Porto, Portugal), David Pereira (CISTER, Polytechnic Institute of Porto, Portugal), Giann Spilere Nandi (CISTER, Polytechnic Institute of Porto, Portugal), Sina Borrami (Alstom), Jonas Melchert (Alstom)
• Abstract summary: This work exploits variability of the formal model being analysed and the requirements being checked, to facilitate the model-checking of variations of real-time specifications. The configuration of the variability of the formal specifications is described in MS Excel spreadsheets with a particular structure, making it easy to use also by developers. We propose the extension of our previous work by exploiting analysis over valid combination of features, while preserving the simplicity of a spreadsheet-based interface with the model checker.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Model checking real-time systems is complex, and requires a careful trade-off between including enough detail to be useful and not too much detail to avoid state explosion. This work exploits variability of the formal model being analysed and the requirements being checked, to facilitate the model-checking of variations of real-time specifications. This work results from the collaboration between academics and Alstom, a railway company with a concrete use-case, in the context of the VALU3S European project. The configuration of the variability of the formal specifications is described in MS Excel spreadsheets with a particular structure, making it easy to use also by developers. These spreadsheets are processed automatically by our prototype tool that generates instances and runs the model checker. We propose the extension of our previous work by exploiting analysis over valid combination of features, while preserving the simplicity of a spreadsheet-based interface with the model checker.

Related papers

• A Simple Baseline for Predicting Events with Auto-Regressive Tabular Transformers [70.20477771578824]
  Existing approaches to event prediction include time-aware positional embeddings, learned row and field encodings, and oversampling methods for addressing class imbalance. We propose a simple but flexible baseline using standard autoregressive LLM-style transformers with elementary positional embeddings and a causal language modeling objective. Our baseline outperforms existing approaches across popular datasets and can be employed for various use-cases.
  arXiv  Detail & Related papers  (2024-10-14T15:59:16Z)
• Multi-Grained Specifications for Distributed System Model Checking and Verification [9.14614889088682]
  We use TLA+ to model fine-grained behaviors of ZooKeeper and the TLC model checker to verify its correctness properties. We show that writing multi-grained specifications is a viable practice and can cope with model-code gaps without untenable state space.
  arXiv  Detail & Related papers  (2024-09-22T02:59:56Z)
• SpreadsheetBench: Towards Challenging Real World Spreadsheet Manipulation [34.8332394229927]
  SpreadsheetBench is designed to immerse current large language models (LLMs) in the actual workflow of spreadsheet users. Unlike existing benchmarks that rely on synthesized queries and simplified spreadsheet files, SpreadsheetBench is built from 912 real questions gathered from online Excel forums. Our comprehensive evaluation of various LLMs under both single-round and multi-round inference settings reveals a substantial gap between the state-of-the-art (SOTA) models and human performance.
  arXiv  Detail & Related papers  (2024-06-21T09:06:45Z)
• A General Model for Aggregating Annotations Across Simple, Complex, and Multi-Object Annotation Tasks [51.14185612418977]
  A strategy to improve label quality is to ask multiple annotators to label the same item and aggregate their labels. While a variety of bespoke models have been proposed for specific tasks, our work is the first to introduce aggregation methods that generalize across many diverse complex tasks. This article extends our prior work with investigation of three new research questions.
  arXiv  Detail & Related papers  (2023-12-20T21:28:35Z)
• Quantifying Language Models' Sensitivity to Spurious Features in Prompt Design or: How I learned to start worrying about prompt formatting [68.19544657508509]
  Large language models (LLMs) are adopted as a fundamental component of language technologies. We find that several widely used open-source LLMs are extremely sensitive to subtle changes in prompt format in few-shot settings. We propose an algorithm that rapidly evaluates a sampled set of plausible prompt formats for a given task, and reports the interval of expected performance without accessing model weights.
  arXiv  Detail & Related papers  (2023-10-17T15:03:30Z)
• 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)
• Improving Text Matching in E-Commerce Search with A Rationalizable, Intervenable and Fast Entity-Based Relevance Model [78.80174696043021]
  We propose a novel model called the Entity-Based Relevance Model (EBRM) The decomposition allows us to use a Cross-encoder QE relevance module for high accuracy. We also show that pretraining the QE module with auto-generated QE data from user logs can further improve the overall performance.
  arXiv  Detail & Related papers  (2023-07-01T15:44:53Z)
• Merlion: A Machine Learning Library for Time Series [73.46386700728577]
  Merlion is an open-source machine learning library for time series. It features a unified interface for models and datasets for anomaly detection and forecasting. Merlion also provides a unique evaluation framework that simulates the live deployment and re-training of a model in production.
  arXiv  Detail & Related papers  (2021-09-20T02:03:43Z)
• DirectDebug: Automated Testing and Debugging of Feature Models [55.41644538483948]
  Variability models (e.g., feature models) are a common way for the representation of variabilities and commonalities of software artifacts. Complex and often large-scale feature models can become faulty, i.e., do not represent the expected variability properties of the underlying software artifact.
  arXiv  Detail & Related papers  (2021-02-11T11:22:20Z)
• IFC models for (semi)automating common planning checks for building permits [0.0]
  A tool was developed to extract the necessary information from IFC models to check representative regulations. While the case study is specific in location, regulations and input models, the type of issues encountered are a generally applicable example for automated code compliance checking.
  arXiv  Detail & Related papers  (2020-11-03T15:29:47Z)

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.