Abstract

Abstract
Embedding CRDT counters has shown to be a challenging topic, since their introduction in Riak Maps. The desire for obliviousness, where all information about a counter is fully removed upon key removal, faces problems due to the possibility of concurrency between increments and key removals. Previous state-based proposals exhibit undesirable reset-wins semantics, which lead to losing increments, unsatisfactorily solved through manual generation management in the API. Previous operation-based approaches depend on causal stability, being prone to unbounded counter growth under network partitions. We introduce a novel embeddable operation-based CRDT counter which achieves both desirable observed-reset semantics and obliviousness upon resets. Moreover, it achieves this while merely requiring FIFO delivery, allowing a tradeoff between causal consistency and faster information propagation, being more robust under network partitions.

Abstract
TCP is typically the default transport protocol of choice for its supposed reliability, even for message-oriented middleware (e.g., ZeroMQ) or inter-actor communication (e.g., distributed Erlang). However, under network issues, TCP connections can fail, which requires ensuring both at-least-once and at-most-once delivery at the upper middleware layer. Moreover, the use of TCP at scale, in highly concurrent systems, can lead to drastic performance loss due to the need for TCP connection multiplexing and the resulting head-of-line blocking. This paper introduces Exon, an oblivious exactly-once messaging protocol, and a corresponding lightweight library implementation. Exon uses a novel strategy of a per-message four-way protocol to ensure oblivious exactly-once messaging, with on-demand protocol-level soft half-connections that are established when needed and safely discarded. This achieves correctness, obliviousness, and performance, through merging and pipelining basic protocol messages. The empirical evaluation of Exon demonstrates significant improvements in throughput and latency under packet loss, while maintaining a negligible overhead over TCP in healthy networks.

Abstract
Likewise to code, clone-and-own is a common way to create variants of a model, to explore the impact of different features while exploring the design of a software system. Previously, we have introduced Colorful Alloy, an extension of the popular Alloy language and toolkit to support feature-oriented design, where model elements can be annotated with feature expressions and further highlighted with different colors to ease understanding. In this paper we propose a catalog of refactoring laws for Colorful Alloy models, and show how they can be used to iteratively merge cloned Alloy models into a single featureannotated colorful model, where the commonalities and differences between the different clones are easily perceived, and more efficient aggregated analyses can be performed. We then show how these refactorings can be composed in an automated merging strategy that can be used to migrate Alloy clones into a Colorful Alloy SPL in a single step. The paper extends a conference version [1] by formalizing the semantics and type system of the improved Colorful Alloy language, allowing the simplification of some rules and the evaluation of their soundness. Additional rules were added to the catalog, and the evaluation extended. The automated merging strategy is also novel.

Abstract
Effective testing of message-oriented software requires describing the expected behaviour of the system and the causality relations between messages. This is often achieved with formal specifications based on temporal logics that require both first-order and metric temporal constructs - to specify constraints over data and real time. This paper proposes a technique to automatically generate tests for metric first-order temporal specifications that match well-understood specification patterns. Our approach takes in properties in a high-level specification language and identifies test schemas (strategies) that are likely to falsify the property. Schemas correspond to abstract classes of execution traces, that can be refined by introducing assumptions about the system. At the low level, concrete traces are successively produced for each schema using property-based testing principles. We instantiate this approach for a popular robotic middleware, ROS, and evaluate it on two systems, showing that schema-based test generation is effective for message-oriented software.

Abstract
This paper proposes the first mutation-based technique for the repair of Alloy 6 first-order temporal logic specifications. This technique was developed with the educational context in mind, in particular, to repair submissions for specification challenges, as allowed, for example, in the Alloy4Fun web-platform. Given an oracle and an incorrect submission, the proposed technique searches for syntactic mutations that lead to a correct specification, using previous counterexamples to quickly prune the search space, thus enabling timely feedback to students. Evaluation shows that, not only is the technique feasible for repairing temporal logic specifications, but also outperforms existing techniques for non-temporal Alloy specifications in the context of educational challenges.