-
Validating Labelled State Transition and Message Production Systems: A Theory for Modelling Faulty Distributed Systems
Authors:
Vlad Zamfir,
Mihai Calancea,
Denisa Diaconescu,
Wojciech Kołowski,
Brandon Moore,
Karl Palmskog,
Traian Florin Şerbănuţă,
Michael Stay,
Dafina Trufaş,
Jan Tušil
Abstract:
Modeling and formally reasoning about distributed systems with faults is a challenging task. To address this problem, we propose the theory of Validating Labeled State transition and Message production systems (VLSMs). The theory of VLSMs provides a general approach to describing and verifying properties of distributed protocols whose executions are subject to faults, supporting a correct-by-const…
▽ More
Modeling and formally reasoning about distributed systems with faults is a challenging task. To address this problem, we propose the theory of Validating Labeled State transition and Message production systems (VLSMs). The theory of VLSMs provides a general approach to describing and verifying properties of distributed protocols whose executions are subject to faults, supporting a correct-by-construction system development methodology. The central focus of our investigation is equivocation, a mode of faulty behavior that we formally model, reason about, and then show how to detect from durable evidence that may be available locally to system components. Equivocating components exhibit behavior that is inconsistent with single-trace system executions, while also only interacting with other components by sending and receiving valid messages. Components of system are called validators for that system if their validity constraints validate that the messages they receive are producible by the system. Our main result shows that for systems of validators, the effect that Byzantine components can have on honest validators is precisely identical to the effect that equivocating components can have on non-equivocating validators. Therefore, for distributed systems of potentially faulty validators, replacing Byzantine components with equivocating components has no material analytical consequences, and forms the basis of a sound alternative foundation to Byzantine fault tolerance analysis. All of the results and examples in the paper have been formalised and checked in the Coq proof assistant.
△ Less
Submitted 15 December, 2023; v1 submitted 25 February, 2022;
originally announced February 2022.
-
Many-Sorted Hybrid Modal Languages
Authors:
Ioana Leuştean,
Natalia Moangă,
Traian Florin Şerbănuţă
Abstract:
We continue our investigation into hybrid polyadic multi-sorted logic with a focus on expresivity related to the operational and axiomatic semantics of rogramming languages, and relations with first-order logic. We identify a fragment of the full logic, for which we prove sound and complete deduction and we show that it is powerful enough to represent both the programs and their semantics in an un…
▽ More
We continue our investigation into hybrid polyadic multi-sorted logic with a focus on expresivity related to the operational and axiomatic semantics of rogramming languages, and relations with first-order logic. We identify a fragment of the full logic, for which we prove sound and complete deduction and we show that it is powerful enough to represent both the programs and their semantics in an uniform way. Although weaker than other hybrid systems previously developed, this system is expected to have better computational properties. Finally, we provide a standard translation from full hybrid many-sorted logic to first-order logic.
△ Less
Submitted 2 July, 2020;
originally announced July 2020.
-
From Hybrid Modal Logic to Matching Logic and Back
Authors:
Ioana Leuştean,
Natalia Moangă,
Traian Florin Şerbănuţă
Abstract:
Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provides a rigorous way to transfer results between the two approaches, which should benefit both systems.
Building on our previous work on hybrid polyadic modal logic we identify modal logic equivalents for Matching Logic, a logic for program specification and verification. This provides a rigorous way to transfer results between the two approaches, which should benefit both systems.
△ Less
Submitted 4 September, 2019; v1 submitted 11 July, 2019;
originally announced July 2019.
-
Operational semantics and program verification using many-sorted hybrid modal logic
Authors:
Ioana Leustean,
Natalia Moanga,
Traian Florin Serbanuta
Abstract:
We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal logic, for which we prove completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (…
▽ More
We propose a general framework to allow: (a) specifying the operational semantics of a programming language; and (b) stating and proving properties about program correctness. Our framework is based on a many-sorted system of hybrid modal logic, for which we prove completeness results. We believe that our approach to program verification improves over the existing approaches within modal logic as (1) it is based on operational semantics which allows for a more natural description of the execution than Hoare's style weakest precondition used by dynamic logic; (2) being multi-sorted, it allows for a clearer encoding of semantics, with a smaller representational distance to its intended meaning.
△ Less
Submitted 13 May, 2019;
originally announced May 2019.
-
All-Path Reachability Logic
Authors:
Andrei Stefanescu,
Stefan Ciobaca,
Radu Mereuta,
Brandon Moore,
Traian Florin Serbanuta,
Grigore Rosu
Abstract:
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof…
▽ More
This paper presents a language-independent proof system for reachability properties of programs written in non-deterministic (e.g., concurrent) languages, referred to as all-path reachability logic. It derives partial-correctness properties with all-path semantics (a state satisfying a given precondition reaches states satisfying a given postcondition on all terminating execution paths). The proof system takes as axioms any unconditional operational semantics, and is sound (partially correct) and (relatively) complete, independent of the object language. The soundness has also been mechanized in Coq. This approach is implemented in a tool for semantics-based verification as part of the K framework (http://kframework.org)
△ Less
Submitted 29 April, 2019; v1 submitted 25 October, 2018;
originally announced October 2018.
-
A many-sorted polyadic modal logic
Authors:
Ioana Leustean,
Natalia Moanga,
Traian Florin Serbanuta
Abstract:
This paper presents a many-sorted polyadic modal logic that generalizes some of the existing approaches. The algebraic semantics has led us to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the Jónsson-Tarski theorem. While the transition from the mono-sorted logic to many-sorted one is a smooth process, we see our system as a step towards deepe…
▽ More
This paper presents a many-sorted polyadic modal logic that generalizes some of the existing approaches. The algebraic semantics has led us to a many-sorted generalization of boolean algebras with operators, for which we prove the analogue of the Jónsson-Tarski theorem. While the transition from the mono-sorted logic to many-sorted one is a smooth process, we see our system as a step towards deepening the connection between modal logic and program verification, since our system can be seen as the propositional fragment of Matching logic, a first-order logic for specifying and reasoning about programs.
△ Less
Submitted 30 November, 2018; v1 submitted 26 March, 2018;
originally announced March 2018.
