Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications

• URL: http://arxiv.org/abs/2309.09148v1
• Date: Sun, 17 Sep 2023 03:43:25 GMT
• Title: Rely-guarantee Reasoning about Concurrent Reactive Systems: The PiCore Framework, Languages Integration and Applications
• Authors: Yongwang Zhao, David Sanan
• Abstract summary: This article proposes PiCore, a rely-guarantee reasoning framework for formal specification and verification of CRSs. We design an event specification language supporting complex reaction structures and its rely-guarantee proof system to detach the specification and logic of reactive aspects of CRSs from event behaviours. By this design, we have successfully integrated two existing languages and their rely-guarantee proof systems without any change of their specification and proofs.
• Score: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: The rely-guarantee approach is a promising way for compositional verification of concurrent reactive systems (CRSs), e.g. concurrent operating systems, interrupt-driven control systems and business process systems. However, specifications using heterogeneous reaction patterns, different abstraction levels, and the complexity of real-world CRSs are still challenging the rely-guarantee approach. This article proposes PiCore, a rely-guarantee reasoning framework for formal specification and verification of CRSs. We design an event specification language supporting complex reaction structures and its rely-guarantee proof system to detach the specification and logic of reactive aspects of CRSs from event behaviours. PiCore parametrizes the language and its rely-guarantee system for event behaviour using a rely-guarantee interface and allows to easily integrate 3rd-party languages via rely-guarantee adapters. By this design, we have successfully integrated two existing languages and their rely-guarantee proof systems without any change of their specification and proofs. PiCore has been applied to two real-world case studies, i.e. formal verification of concurrent memory management in Zephyr RTOS and a verified translation for a standardized Business Process Execution Language (BPEL) to PiCore.

Related papers

• Conversation Routines: A Prompt Engineering Framework for Task-Oriented Dialog Systems [0.21756081703275998]
  This study introduces Conversation Routines (CR), a structured prompt engineering framework for developing task-oriented dialog systems using Large Language Models (LLMs) The proposed CR framework enables the development of Conversation Agentic Systems (CAS) through natural language specifications. We demonstrate the framework's effectiveness through two proof-of-concept implementations: a Train Booking System and an Interactive Ticket Copilot.
  arXiv  Detail & Related papers  (2025-01-20T17:19:02Z)
• SVTRv2: CTC Beats Encoder-Decoder Models in Scene Text Recognition [77.28814034644287]
  We propose SVTRv2, a CTC model that beats leading EDTRs in both accuracy and inference speed. SVTRv2 introduces novel upgrades to handle text irregularity and utilize linguistic context. We evaluate SVTRv2 in both standard and recent challenging benchmarks.
  arXiv  Detail & Related papers  (2024-11-24T14:21:35Z)
• Securing Legacy Communication Networks via Authenticated Cyclic Redundancy Integrity Check [98.34702864029796]
  We propose Authenticated Cyclic Redundancy Integrity Check (ACRIC) ACRIC preserves backward compatibility without requiring additional hardware and is protocol agnostic. We show that ACRIC offers robust security with minimal transmission overhead ( 1 ms)
  arXiv  Detail & Related papers  (2024-11-21T18:26:05Z)
• A SAT-based approach to rigorous verification of Bayesian networks [13.489622701621698]
  We introduce a verification framework tailored for Bayesian networks, designed to address these drawbacks. Our framework comprises two key components: (1) a two-step compilation and encoding scheme that translates Bayesian networks into Boolean logic literals, and (2) formal verification queries that leverage these literals to verify various properties encoded as constraints. We benchmark the efficiency of our verification scheme and demonstrate its practical utility in real-world scenarios.
  arXiv  Detail & Related papers  (2024-08-02T03:06:51Z)
• Towards interfacing large language models with ASR systems using confidence measures and prompting [54.39667883394458]
  This work investigates post-hoc correction of ASR transcripts with large language models (LLMs) To avoid introducing errors into likely accurate transcripts, we propose a range of confidence-based filtering methods. Our results indicate that this can improve the performance of less competitive ASR systems.
  arXiv  Detail & Related papers  (2024-07-31T08:00:41Z)
• Joint vs Sequential Speaker-Role Detection and Automatic Speech Recognition for Air-traffic Control [60.35553925189286]
  We propose a transformer-based joint ASR-SRD system that solves both tasks jointly while relying on a standard ASR architecture. We compare this joint system against two cascaded approaches for ASR and SRD on multiple ATC datasets.
  arXiv  Detail & Related papers  (2024-06-19T21:11:01Z)
• Rely-guarantee Reasoning about Concurrent Memory Management: Correctness, Safety and Security [0.0]
  An incorrect specification and implementation of the memory management may lead to system crashes or exploitable attacks. This article presents the first formal specification and mechanized proof of a concurrent memory management for a real-world OS.
  arXiv  Detail & Related papers  (2023-09-17T03:41:10Z)
• Event-based Compositional Reasoning of Information-Flow Security for Concurrent Systems [5.965840906609809]
  We propose a rely-guarantee-based compositional reasoning approach for information-flow security (IFS) for concurrent systems. We first design a language by incorporating Event'' into concurrent languages and give the IFS semantics of the language. For compositional reasoning of IFS, we use rely-guarantee specification to define new forms of unwinding conditions (UCs) on events.
  arXiv  Detail & Related papers  (2023-09-17T02:57:05Z)
• Conformance Checking for Pushdown Reactive Systems based on Visibly Pushdown Languages [0.0]
  Testing pushdown reactive systems is deemed important to guarantee a precise and robust software development process. We show that test suites with a complete fault coverage can be generated using this conformance relation for pushdown reactive systems.
  arXiv  Detail & Related papers  (2023-08-14T14:37:43Z)
• Monitoring ROS2: from Requirements to Autonomous Robots [58.720142291102135]
  This paper provides an overview of a formal approach to generating runtime monitors for autonomous robots from requirements written in a structured natural language. Our approach integrates the Formal Requirement Elicitation Tool (FRET) with Copilot, a runtime verification framework, through the Ogma integration tool.
  arXiv  Detail & Related papers  (2022-09-28T12:19:13Z)
• The Whole Truth and Nothing But the Truth: Faithful and Controllable Dialogue Response Generation with Dataflow Transduction and Constrained Decoding [65.34601470417967]
  We describe a hybrid architecture for dialogue response generation that combines the strengths of neural language modeling and rule-based generation. Our experiments show that this system outperforms both rule-based and learned approaches in human evaluations of fluency, relevance, and truthfulness.
  arXiv  Detail & Related papers  (2022-09-16T09:00:49Z)

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.