Solid foundations for the next generation of communication-based software systems
Analysis techniques based on formal models of communication help to eliminate the errors in software systems that rely on communicating artefacts.
From e-banking and e-commerce services to social networks and content-sharing platforms, distributed software systems pervade our lives. These systems are typically built by aggregating software artefacts (e.g., mobile apps, Web services and legacy components), which are written in different programming languages and executed in various platforms. To achieve their goals, these artefacts use communication protocols. Ensuring that communication-based software systems behave as intended is both challenging and crucial, due to their large societal impact..
We investigate rigorous models that are capable of distilling the essence of communication-based software. We then use these models to build analysis techniques that may help developers remove bugs from communicating programs.
Framed within the grand challenge of ensuring software correctness, we use techniques that originate from programming languages, concurrency theory and logic. Ensuring that a collection of distributed software artefacts will execute a given communication protocol correctly represents a long-standing challenge. There are two key obstacles to achieving this aim. First, because mainstream programming languages lack mechanisms for describing communication structures, external protocol descriptions are required for program validation. Second, our models need to account for the possibility that protocols and/or artefacts may change during runtime.
Our work tackles these challenges using type systems. Type systems offer analysis techniques in which each program value is associated with a type (say, a string or integer). We use ‘behavioural types’ to classify the behaviour of a communicating program with respect to a governing protocol. Behavioural types define abstract protocol descriptions. By using type-checking techniques to examine a program’s text, we may detect communication bugs and errors. Behavioural types are coupled to core models of communication that describe basic interactions. Our research therefore helps develop a better understanding of both of these communication models and their associated behavioural types.
‘Session types’ are a class of behavioural type that abstracts communication protocols into units called sessions. A session describes the order and content of reciprocal communication actions. For instance, the session type
describes a protocol that first sends (!) a value of type string, then receives (?) a value of type int, and then closes the protocol. Session types are developed on top of process calculi, which are models of communication that precisely specify communicating programs. Using process calculi and session types, we can establish the correctness properties of interacting processes in a rigorous way. These properties may then be transferred to full-blown programming languages.
We have studied foundations for session types from a variety of perspectives. First, we have helped develop correspondences between session types and linear logic (a resource-aware logic). These correspondences define new logical foundations for concurrent programming. We have also investigated the expressive power (i.e., the breadth of ideas that can be represented and communicated) of the expressive power of session-type frameworks, i.e., the kind of communicating systems that can be represented and reasoned about in those models. Our goal is to identify useful connections between differently typed frameworks, so as to enable transfer analysis techniques between them. Finally, we have proposed the first session-type framework with mechanisms for runtime adaptation. This framework includes new process-calculi constructs and formal characterizations of communication correctness in highly dynamic settings.
Our interest in integrating runtime adaptation into session-type frameworks follows two directions. First, we investigate process languages with constructs representing dynamic updates for running processes. We then integrate standard session-type disciplines on top of these languages. Our intention is to explicitly distinguish adaptation requirements (specified by processes) from communication protocols (specified by session types). A tension exists between the execution of runtime adaptation steps and the enforcement of correct communication protocols. To ensure a safe interplay between these two concerns, we identified consistent adaptation steps (i.e., runtime modifications of process behaviours that respect the protocols prescribed by session types).
In the second approach, runtime adaptation requirements are connected with the security properties of the system. For this, we consider a model of interacting processes in which runtime adaptation is triggered in response to security leaks. The targeted properties are information flow and access control. The session protocol is used to obtain a session monitor for each participant, which enables its communicating actions (input and output) to take place according to the associated security permissions. Adaptation actions depend on the gravity of security leaks. For minor leaks, unauthorized actions are ignored and the protocol proceeds, whereas major security leaks may lead to a complete update of the session protocol.
As the societal impact of communication-based software systems grows, the need for solid foundations that enable their principled construction becomes more pronounced. By building upon behavioural types and formal models of communication, we have developed techniques that help to ensure correct communicating programs. The integration of analysis techniques that are based on behavioural types for application in approaches to verification of collective adaptive systems represents an interesting challenge as both approaches exhibit clear complementarities. Extensions of type-based techniques with distinctive features in collective adaptive systems (e.g., autonomous behaviour, self-awareness, knowledge management and quantitative reasoning) should enable the analysis of a larger, high-impact class of communication-based software systems.
The papers mentioned/described in this article have been developed in cooperation with the following people, from whom I have learnt a lot: Luís Caires, Mauricio Cano, Ilaria Castellani, Ornela Dardha, Mariangiola Dezani-Ciancaglini, Cinzia Di Giusto, Hugo Lopez, Frank Pfenning, Camilo Rueda and Bernardo Toninho. The support of EU COST Action IC1201: Behavioural Types for Reliable Large-Scale Software Systems (BETTY) is also acknowledged with gratitude.
- K. Honda, V. T. Vasconcelos and M. Kubo, Language primitives and type discipline for structured communication-based programming, Proc. ESOP, pp. 122–138, 1998.
- J. A. Pérez, L. Caires, F. Pfenning and B. Toninho, Linear logical relations and observational equivalences for session-based concurrency, Inf. Comput. 239, pp. 254–302, 2014.
- L. Caires and F. Pfenning, Session types as intuitionistic linear propositions, Proc. CONCUR 6269, pp. 222–236, 2010.
- O. Dardha and J. A. Pérez, Comparing deadlock-free session typed processes, Proc. EXPRESS/SOS 190, pp. 1–15, 2015.
- M. Cano, C. Rueda, H. A. López and J. A. Pérez, Declarative interpretations of session-based concurrency, Proc. 17th Int’l Symp. PPDP, pp. 67–78, 2015.
- C. Di Giusto and J. A. Pérez, Disciplined structured communications with disciplined runtime adaptation, Sci. Comput. Program. 97, pp. 235–265, 2015.
- I. Castellani, M. Dezani-Ciancaglini, and J. A. Pérez, Self-adaptation and secure information flow in multiparty structured communications: a unified perspective, Proc. BEAT 162, pp. 9–18, 2014.