Search papers, labs, and topics across Lattice.
This paper introduces an extension to typestates called Mixed-Choice Stateful Typestates to better model and verify distributed applications. The extension incorporates internal mutable state for quantitative constraints, mixed sessions for concurrent I/O, and expected ratios for action counts, addressing limitations of traditional typestates. A probabilistic runtime monitoring solution is presented to detect deviations from expected behavior, improving the robustness of distributed protocols.
Traditional typestates fall short in modeling complex distributed systems, but this work introduces a novel extension that captures quantitative constraints and concurrent I/O, enabling more accurate verification.
Distributed systems have become increasingly prevalent in the software industry. Due to their intrinsic complexity, much research has focused on the verification of their behaviour. An active research line is around behaviour models that capture these protocols - e.g., session types, or typestates - allowing their static verification. Correctly designing distributed protocols is not trivial. Their communication behaviour is typically implicitly defined via asynchronous message handlers, making errors harder to detect until execution. While typestates can ease the design process by explicitly defining correct sequences of operations, they struggle in two ways: they lack the expressiveness to define quantitative constraints that govern distributed protocols (i.e., number of acknowledgements for a quorum); and they assume strict sequencing of operations, failing to capture concurrent input/output actions in a state, typical of the distributed setting. Furthermore, runtime network failures cannot be statically verified. We present a probabilistic runtime solution extending typestates with: (i) an internal mutable state for the expression of quantitative constraints; (ii) mixed sessions to represent concurrent input and output actions; (iii) expected ratios for the number of actions in a state, with monitoring semantics to detect deviations from an expected behaviour at runtime. We demonstrate the suitability of our solution with two examples that motivated our approach: an acknowledgement protocol with a participant that sends several messages while waiting for a response, effectively modelling input and output operations in a state; and a voting protocol whose participants try to achieve consensus on a single bit using a quorum, thus, requiring an internal mutable state, while respecting a pre-defined distribution for the volume of exchanged messages.
