Runtime Verification (RV) is gaining popularity due to its scalability and ability to analyse block-box systems. Monitoring is at the heart of RV; a logical formula ϕ, formalising some property of interest, is typically translated into a monitor that checks whether the system under scrutiny satisfies ϕ during its execution. A logical formula ϕ is violation (resp. satisfaction) monitorable iff there exists a monitor for ϕ that is both sound and complete w.r.t. its violation (resp. satisfaction). The monitorability problem is thus concerned with determining the largest subset of a logic L that is monitorable. Although this problem has been solved for expressive untimed logics, it remains open for timed logics, where formulae can express both the order of events and the quantity of time separating them. This paper solves the monitorability problem for T^lin, a new expressive (linear-time) timed μ-calculus that we propose. First, we show that T^lin is strictly more expressive than MTL, the de facto timed extension of LTL. Second, we identify MT^lin, the largest monitorable fragment of T^lin: we characterise its largest subsets of formulae that are violation monitorable, satisfaction monitorable, and complete monitorable (both satisfaction and violation monitorable). To wit, this is the first work that answers the monitorability question for such an expressive timed logic.

Abstract De Nicola and Hennessy’s $$\textsc {must}$$ M U S T -preorder is a liveness preserving refinement which states that a server $$q$$ q refines a server $$p$$ p if all clients satisfied by $$p$$ p are also satisfied by $$q$$ q . Owing to the universal quantification over clients, this definition does not yield a practical proof method, and alternative characterisations are necessary to reason over it. Finding these characterisations for asynchronous semantics, i.e. where outputs are non-blocking, has thus far proven to be a challenge, usually tackled via ad-hoc definitions. We show that the standard characterisations of the $$\textsc {must}$$ M U S T -preorder carry over as they stand to asynchronous communication, if servers are enhanced to act as forwarders, i.e. they can input any message as long as they store it back into the shared buffer. Our development is constructive, is completely mechanised in Coq, and is independent of any calculus: our results pertain to Selinger output-buffered agents with feedback. This is a class of Labelled Transition Systems that captures programs that communicate via a shared unordered buffer, as in asynchronous CCS or the asynchronous $$\pi $$ π -calculus. We show that the standard coinductive characterisation lets us prove in Coq that concrete programs are related by the $$\textsc {must}$$ M U S T -preorder. Finally, our proofs show that Brouwer’s bar induction principle is a useful technique to reason on liveness preserving program transformations.

To achieve scalability, modern Internet services often rely on distributed databases with consistency models for transactions weaker than serializability. At present, application programmers often lack techniques to ensure that the weakness of these consistency models does not violate application correctness. We present criteria to check whether applications that rely on a database providing only weak consistency are robust, i.e., behave as if they used a database providing serializability. When this is the case, the application programmer can reap the scalability benefits of weak consistency while being able to easily check the desired correctness properties. Our results handle systematically and uniformly several recently proposed weak consistency models, as well as a mechanism for strengthening consistency in parts of an application.

Session types and contracts are two formalisms used to study client–server protocols. In this paper, we study the relationship between them. The main result is the existence of a fully abstract model of session types; this model is based on a natural interpretation of these types into a subset of contracts.

Modern distributed systems often rely on databases that achieve scalability by providing only weak guarantees about the consistency of distributed transaction processing. The semantics of programs interacting with such a database depends on its consistency model, defining these guarantees. Unfortunately, consistency models are usually stated informally or using disparate formalisms, often tied to the database internals. To deal with this problem, we propose a framework for specifying a variety of consistency models for transactions uniformly and declaratively. Our specifications are given in the style of weak memory models, using structures of events and relations on them. The specifications are particularly concise because they exploit the property of atomic visibility guaranteed by many consistency models: either all or none of the updates by a transaction can be visible to another one. This allows the specifications to abstract from individual events inside transactions. We illustrate the use of our framework by specifying several existing consistency models. To validate our specifications, we prove that they are equivalent to alternative operational ones, given as algorithms closer to actual implementations. Our work provides a rigorous foundation for developing the metatheory of the novel form of concurrency arising in weakly consistent large-scale databases.