1,721,007 research outputs found
Asynchronous session subtyping as communicating automata refinement
Full text linkWe study the relationship between session types and behavioural contracts, representing Communicating Finite State Machines (CFSMs), under the assumption that processes communicate asynchronously. Session types represent a syntax-based approach for the description of communication protocols, while behavioural contracts, formally expressing CFSMs, follow an operational approach. We show the existence of a fully abstract interpretation of session types into a fragment of contracts that maps session subtyping into binary compliance-preserving CFSMs/behavioural contract refinement. In this way, on the one hand, we enrich the theory of session types with an operational characterization and, on the other hand, we use recent undecidability results for asynchronous session subtyping to obtain an original undecidability result for asynchronous CFSMs/behavioural contract refinement
Discrete Time Generative-Reactive Probabilistic Processes with Different Advancing Speeds
Full text linkWe present a process algebra expressing probabilistic external/internal choices, multi-way synchronizations, and processes with different advancing speeds in the context of discrete time, i.e. where time is not continuous but is represented by a sequence of discrete steps as in discrete time Markov chains (DTMCs). To this end, we introduce a variant of CSP that employs a probabilistic asynchronous parallel operator whose synchronization mechanism is based on a mixture of the classical generative and reactive models of probability. In particular, differently from existing discrete time process algebras, where parallel processes are executed in synchronous locksteps, the parallel operator that we adopt allows processes with different probabilistic advancing speeds (mean number of actions executed per time unit) to be modeled. Moreover, our generative-reactive synchronization mechanism makes it possible to always derive DTMCs in the case of fully specified systems. We then present a sound and complete axiomatization of probabilistic bisimulation over finite processes of our calculus, that is a smooth extension of the axiom system for a standard process algebra, thus solving the open problem of cleanly axiomatizing action restriction in the generative model. As a further result, we show that, when evaluating steady state based performance measures which are expressible by attaching rewards to actions, our approach provides an exact solution even if the advancing speeds are considered not to be probabilistic, without incurring the state space explosion problem that arises with standard synchronous approaches. We finally present a case study on multi-path routing showing the expressiveness of our calculus and that it makes it particularly easy to produce scalable specifications
Process calculi as a tool for studying coordination, contracts and session types
Full text linkWe recall techniques, mainly based on the theory of process calculi, that we used to prove results in twenty years of research, spanning across the old and the new millennium, on the expressiveness of coordination languages and on behavioural contracts for Service-Oriented Computing. Then, we show how such techniques recently contributed to the clarification of aspects that were unclear about session types, in particular, asynchronous session subtyping that was considered decidable since 2009, while it was proved to be undecidable in 2017
Relating Session Types and Behavioural Contracts: The Asynchronous Case
Full text linkWe discuss the relationship between session types and behavioural contracts under the assumption that processes communicate asynchronously. We show the existence of a fully abstract interpretation of session types into a fragment of contracts, that maps session subtyping into binary compliance-preserving contract refinement. In this way, the recent undecidability result for asynchronous session subtyping can be used to obtain an original undecidability result for asynchronous contract refinement
Non-determinism in Probabilistic Timed Systems with General Distributions
No full textAbstractIn this paper we address the problem of adequately handling non-deterministic choices in Generalised Semi-Markov Processes (GSMPs), i.e. probabilistic timed systems where durations of delays are expressed by means of random variables with a general probability distribution. In particular we want the probabilistic duration of a delay not to be decided all at once when the delay starts, but step by step in each system state (in the theory of GSMPs this corresponds to recording spent lifetimes instead of residual lifetimes of delays). In this way an adversary cannot take decisions a priori, based on the knowledge he may get about the future behavior of the system. In order to accomplish this, we consider Interactive Generalised Semi-Markov Processes (IGSMPs). We start by formalizing the class of well-named IGSMP models and the class of Interactive Stochastic Timed Transition Systems (ISTTSs) which are both closed under CSP parallel composition and hiding. Then, we introduce a semantics for IGSMPs which maps well-named IGSMP models onto ISTTSs by recording spent lifetimes of delays. Finally, we show that two weakly bisimilar IGSMPs give rise to two weakly bisimilar semantic models and that our semantic mapping is compositional with respect to both CSP parallel composition and hiding
A Java typestate checker supporting inheritance
Full text linkDetecting programming errors in software is increasingly important, and building tools that
help developers with this task is a crucial area of investigation on which the industry
depends. Leveraging on the observation that in Object-Oriented Programming (OOP) it is
natural to define stateful objects where the safe use of methods depends on their internal
state, we present Java Typestate Checker (JATYC), a tool that verifies Java source code with
respect to typestates. A typestate defines the object’s states, the methods that can be called
in each state, and the states resulting from the calls. The tool statically verifies that when a
Java program runs: sequences of method calls obey to object’s protocols; objects’ protocols
are completed; null-pointer exceptions are not raised; subclasses’ instances respect the
protocol of their superclasses. To the best of our knowledge, this is the first OOP tool that
simultaneously tackles all these aspects
Expressing Processes with Different Action Durations through Probabilities
No full textWe consider a discrete time process algebra capable of (i) modeling processes with different probabilistic advancing speeds (mean number of actions executed per time unit), and (ii) expressing probabilistic external/internal choices and multiway synchronization. We show that, when evaluating steady state based performance measures expressed by associating rewards with actions, such a probabilistic approach provides an exact solution even if advancing speeds are considered not to be probabilistic (i.e. actions of different processes have a different exact duration), without incurring in the state space explosion problem which arises with an intuitive application of a standard synchronous approach. We then present a case study on multi-path routing showing the expressiveness of our calculus and that it makes it particularly easy to produce scalable specifications
A Session Subtyping Tool
Full text linkSession types are becoming popular and have been integrated in several mainstream programming languages. Nevertheless, while many programming languages consider asynchronous fifo channel communication, the notion of subtyping used in session type implementations is the one defined by Gay and Hole for synchronous communication. This might be because there are several notions of asynchronous session subtyping, these notions are usually undecidable, and only recently sound (but not complete) algorithmic characterizations for these subtypings have been proposed. But the fact that the definition of asynchronous session subtyping and the theory behind related algorithms are not easily accessible to non-experts may also prevent further integration. The aim of this paper, and of the tool presented therein, is to make the growing body of knowledge about asynchronous session subtyping more accessible, thus promoting its integration in practical applications of session types
- …
