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
- 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) - HasTEE+ : Confidential Cloud Computing and Analytics with Haskell [50.994023665559496]
Confidential computing enables the protection of confidential code and data in a co-tenanted cloud deployment using specialized hardware isolation units called Trusted Execution Environments (TEEs)
TEEs offer low-level C/C++-based toolchains that are susceptible to inherent memory safety vulnerabilities and lack language constructs to monitor explicit and implicit information-flow leaks.
We address the above with HasTEE+, a domain-specific language (cla) embedded in Haskell that enables programming TEEs in a high-level language with strong type-safety.
arXiv Detail & Related papers (2024-01-17T00:56:23Z) - 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) - A Modular and Adaptive System for Business Email Compromise Detection [0.7490096698922335]
Business Email Compromise (BEC) and spear phishing attacks pose significant challenges to organizations worldwide.
Recent advances in machine learning, particularly in Natural Language Understanding (NLU), offer a promising avenue for combating such attacks.
We present CAPE, a comprehensive and efficient system for BEC detection that has been proven in a production environment for a period of over two years.
arXiv Detail & Related papers (2023-08-21T15:06:02Z) - 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) - Hybrid Rule-Neural Coreference Resolution System based on Actor-Critic
Learning [53.73316523766183]
Coreference resolution systems need to tackle two main tasks.
One task is to detect all of the potential mentions, the other is to learn the linking of an antecedent for each possible mention.
We propose a hybrid rule-neural coreference resolution system based on actor-critic learning.
arXiv Detail & Related papers (2022-12-20T08:55:47Z) - 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) - Towards Dynamic Consistency Checking in Goal-directed Predicate Answer
Set Programming [2.3204178451683264]
We present a variation of the top-down evaluation strategy, termed Dynamic Consistency checking.
This makes it possible to determine when a literal is not compatible with the denials associated to the global constraints in the program.
We have experimentally observed speedups of up to 90x w.r.t. the standard versions of s(CASP)
arXiv Detail & Related papers (2021-10-22T20:38:48Z) - Generalizing Cross-Document Event Coreference Resolution Across Multiple
Corpora [63.429307282665704]
Cross-document event coreference resolution (CDCR) is an NLP task in which mentions of events need to be identified and clustered throughout a collection of documents.
CDCR aims to benefit downstream multi-document applications, but improvements from applying CDCR have not been shown yet.
We make the observation that every CDCR system to date was developed, trained, and tested only on a single respective corpus.
arXiv Detail & Related papers (2020-11-24T17:45: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.