Timed I/O Automata: It is never too late to complete your timed specification theory

• URL: http://arxiv.org/abs/2302.04529v2
• Date: Thu, 13 Jul 2023 07:50:12 GMT
• Title: Timed I/O Automata: It is never too late to complete your timed specification theory
• Authors: Martijn A. Goorden, Kim G. Larsen, Axel Legay, Florian Lorber, Ulrik Nyman, Andrzej Wasowski
• Abstract summary: We develop a complete specification framework for real-time systems using Timed I/O Automata as the specification formalism. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications.
• Score: 3.2441713533645617
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: A specification theory combines notions of specifications and implementations with a satisfaction relation, a refinement relation and a set of operators supporting stepwise design. We develop a complete specification framework for real-time systems using Timed I/O Automata as the specification formalism, with the semantics expressed in terms of Timed I/O Transition Systems. We provide constructs for refinement, consistency checking, logical and structural composition, and quotient of specifications -- all indispensable ingredients of a compositional design methodology. The theory is backed by rigorous proofs and is being implemented in the open-source tool ECDAR.

Related papers

• What makes Models Compositional? A Theoretical View: With Supplement [60.284698521569936]
  We propose a general neuro-symbolic definition of compositional functions and their compositional complexity. We show how various existing general and special purpose sequence processing models fit this definition and use it to analyze their compositional complexity.
  arXiv  Detail & Related papers  (2024-05-02T20:10:27Z)
• Automated Configuration Synthesis for Machine Learning Models: A git-Based Requirement and Architecture Management System [5.095988654970361]
  This work introduces a tool for generating runtime configurations automatically from textual requirements stored as artifacts in git repositories (a.k.a. T-Reqs) alongside the software code. The tool leverages T-Reqs-modelled architectural description to identify relevant configuration properties for the deployment of artificial intelligence (AI)-enabled software systems.
  arXiv  Detail & Related papers  (2024-04-26T08:35:02Z)
• Defining and executing temporal constraints for evaluating engineering artifact compliance [56.08728135126139]
  Process compliance focuses on ensuring that the actual engineering work is followed as closely as possible to the described engineering processes. Checking these process constraints is still a daunting task that requires a lot of manual work and delivers feedback to engineers only late in the process. We present an automated constraint checking approach that can incrementally check temporal constraints across inter-related engineering artifacts upon every artifact change.
  arXiv  Detail & Related papers  (2023-12-20T13:26:31Z)
• Extending Rely-Guarantee thinking to handle Real-Time Scheduling [1.5527108310849955]
  Real-time systems need ways of both requiring progress and relating that progress to some notion of time. This paper extends rely-guarantee ideas to cope with specifications of -- and assumptions about -- real-time schedulers.
  arXiv  Detail & Related papers  (2023-11-30T20:04:30Z)
• Spreadsheet-based Configuration of Families of Real-Time Specifications [0.0]
  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.
  arXiv  Detail & Related papers  (2023-10-31T12:16:56Z)
• A General Framework for Verification and Control of Dynamical Models via Certificate Synthesis [54.959571890098786]
  We provide a framework to encode system specifications and define corresponding certificates. We present an automated approach to formally synthesise controllers and certificates. Our approach contributes to the broad field of safe learning for control, exploiting the flexibility of neural networks.
  arXiv  Detail & Related papers  (2023-09-12T09:37:26Z)
• Universal Information Extraction as Unified Semantic Matching [54.19974454019611]
  We decouple information extraction into two abilities, structuring and conceptualizing, which are shared by different tasks and schemas. Based on this paradigm, we propose to universally model various IE tasks with Unified Semantic Matching framework. In this way, USM can jointly encode schema and input text, uniformly extract substructures in parallel, and controllably decode target structures on demand.
  arXiv  Detail & Related papers  (2023-01-09T11:51:31Z)
• Design Space Exploration and Explanation via Conditional Variational Autoencoders in Meta-model-based Conceptual Design of Pedestrian Bridges [52.77024349608834]
  This paper provides a performance-driven design exploration framework to augment the human designer through a Conditional Variational Autoencoder (CVAE) The CVAE is trained on 18'000 synthetically generated instances of a pedestrian bridge in Switzerland.
  arXiv  Detail & Related papers  (2022-11-29T17:28:31Z)
• Natural Language Processing for Systems Engineering: Automatic Generation of Systems Modelling Language Diagrams [0.10312968200748115]
  An approach is proposed to assist systems engineers in the automatic generation of systems diagrams from unstructured natural language text. The intention is to provide the users with a more standardised, comprehensive and automated starting point onto which subsequently refine and adapt the diagrams according to their needs.
  arXiv  Detail & Related papers  (2022-08-09T19:20:33Z)
• ProQA: Structural Prompt-based Pre-training for Unified Question Answering [84.59636806421204]
  ProQA is a unified QA paradigm that solves various tasks through a single model. It concurrently models the knowledge generalization for all QA tasks while keeping the knowledge customization for every specific QA task. ProQA consistently boosts performance on both full data fine-tuning, few-shot learning, and zero-shot testing scenarios.
  arXiv  Detail & Related papers  (2022-05-09T04:59:26Z)

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.