Wednesday, July 6, 2022

10:00-10:15. Introduction to T-LADIES and to WP1: Language Adaptation. [SlideWP1]
Walter Cazzola (Università degli Studi di Milano)

10:15-10:45. Welcome to the family, son!
Luca Favalli (Università degli Studi di Milano)

Abstract. Domain-specific languages (DSL) are programming languages capable of expressing aspects and abstractions of a specific application domain. DSLs are designed to suit the needs of domain experts, so that they can directly be involved with the development of complex systems. As a result, DSLs—as most modern software systems—must fulfill the needs of a ever-growing and diverse customer base. In this context, the engineering effort should be directed towards reuse of existing artifacts and maintainability. To achieve this goal, researchers and practictioners took inspiration from the popularity of product line engineering in industrial production and applied similar techniques to the development of variability-aware software systems and programming languages, thus introducing software product lines (SPL) and language product lines (LPL) respectively. In LPLs, language families and their members (language variants) are described in terms of the features they provide—i.e., a configuration with respect to an abstract description of the family, such as a feature model. Despite its popularity and effectiveness, product line development demands steep investments in terms of expertise and technology; it involves several activities: domain analysis, domain implementation, requirement analysis and product derivation. Each activity deals with complex objects, since the number of members of a language family is exponential with respect to the number of features in the feature model. Checking the validity of each variant is often unfeasible, therefore the quality must be ensured on each individual feature, otherwise the development effort may end up being wasted as the LPL becomes less maintainable over time. In this presentation, we will discuss a design methodology for LPLs, including any technological support to the development of language features, design techniques and tools towards their reuse, and the quality assessment of language artifacts and language variants.

Joint work with Walter Cazzola.

[Slide01]

10:45-11:15. Hydra: a source-to-source, one-to-many, transpiler infrastructure.
Francesco Bertolotti (Università degli Studi di Milano)

Abstract. Often software ecosystems around each programming language evolve independently from each other. As a result, many functionally similar libraries are continuously rewritten in different languages to satisfy the needs of different developers. However, this degree of replication is undesirable as it forces developers to learn new interfaces every time they switch languages. Moreover, it leads to inconsistent interfaces between different ecosystems, resulting in different solutions for the same problems. The development of language-independent libraries can help to create a set of core functionalities shared among all languages. However, to do so, it is necessary to be able to port these libraries to any language easily. In this work, we present Hydra. Hydra is a source-to-source, one-to-many, extensible transpiler to develop language-independent libraries. Hydra libraries are developed using HydraKernel, a subset of the Scala language. HydraKernel sources are translated to target languages for which an HydraTemplate is available. HydraTemplates guide the translation of HydraKernel sources into the target languages equivalent. HydraTemplates define target languages in a declarative way, so that, the development effort is minimal while maintaining a high degree of reusability. Ultimately, Hydra provides the infrastructure to define transpilers from HydraKernel to other languages in a reusable and extensible way.

Joint work with Walter Cazzola, Dario Ostuni and Carlo Castoldi.

[Slide02]

11:15-11:45. Coffee Break.

11:45-12:15. Towards abstract and (hopefully) compositional operational reasoning.
Francesco Dagnino (Università degli Studi di Genova)

Abstract. Operational semantics is one of the most popular techniques to formally describe the semantics of a programming language, providing a basis for formal reasoning on the behaviour of programs. However, operational models and the associated techniques are typically tailored to specific (families of) languages. As a consequence, they often lack generality and modularity, with the result that for each new model one has to basically redo a lot of work from scratch. In this talk, I will outline a line of research aiming at developing operational semantics and techniques in the abstract, so that they can be applied to large classes of languages. We focus on two styles of operational semantics: big-step semantics and evaluation semantics. In the former case, using proof-theoretic techniques, we describe a general proof technique for type soundness. In the latter case, exploiting categorical tools, we give a general account of logical relations for effectful languages, covering also recently introduced differential logical relations.

This is the result of joint works with many people: Davide Ancona, Viviana Bono, Mariangiola Dezani, Francesco Gavazzo, Jurriaan Rot and Elena Zucca.

[Slide03]

12:15-12:45. Source-to-source, many-to-many, transpiler infrastructure using delta-translations.
Francesco Bertolotti (Università degli Studi di Milano)

Abstract. With the Neverlang language workbench, one can develop languages, compilers/interpreters, IDEs, and other tools. However, with time, languages develop their ecosystem of software. Unfortunately, a mature ecosystem requires years of community development before becoming able to cover a large variety of applicative domains. As a result, the adoption of new languages often depends on the maturity of their ecosystems. Therefore, developing tools that can migrate the software ecosystems from one language to another can have a beneficial impact by: 1) speeding up language development, 2) speeding up language adoption, and 3) bringing a shared software ecosystem among languages. To this end, transpilers are promising tools, as translation can render code available from one language to the other with little or no overhead. However, transpilers need to be developed in a reusable and modular, so that, new languages can be supported easily and in a timely manner. By defining a database of translation functions (performing a mapping from AST pieces to others) one can build systems capable of performing entire translations. For example, from C++ to Java. Once the translation functions that map Java to Scala programs are defined, one can automatical transfer software from the C++ ecosystem to Scala through Java. New languages that wish to share an ecosystem with another language need only to define enough translations to bridge a path from the desired ecosystem to the new language.

Joint work with Walter Cazzola.

[Slide04]

12:45-13:15. Non-regular corecursive streams.
Pietro Barbieri (Università degli Studi di Genova)

Abstract. We propose a calculus for processing streams by representing them with finitary equational systems built on top of various operators, besides the standard constructor. Functions defining streams are regularly corecursive, that is, cyclic calls are detected, avoiding non-termination. We present an algorithm to check whether a stream is well-defined, which means that access to an arbitrary element will always return a result and, furthermore, we provide a decidable procedure to state the equality of streams built on different stream operators, including tail operator and constructor, and prove its soundness.

Joint work with Davide Ancona, Elena Zucca

[Slide05]

13:15-13:30. Questions and (Maybe) Answers, Discussion and Brainstorming.

13:30-14:30. Lunch.

14:30-14:45. Introduction to WP4: Applications to IoT.
Alessio Ferrari (ISTI-CNR Pisa) and Corrado Santoro (Università degli Studi di Catania)

14:45-15:15. An Overview of Indoor Positioning for IoT Applications.
Stefania Monica (Università degli Studi di Modena e Reggio Emilia)

Abstract. The first part of this talk motivates the need for indoor positioning in the scope of advanced IoT applications. Then, the positioning problem is discussed, and the peculiarities of indoor positioning are briefly summarized to emphasize the need for specific tools to treat it effectively. Finally, some hints on the possibility of providing specific support for indoor positioning at the programming language level are discussed with specific regard to software agents and agent-oriented programming languages.

[Slide06]

15:15-15:45. Human factors evaluation in IoT software design and implementation.
Giovanna Broccia (ISTI-CNR Pisa)

Abstract. Albeit human factors have obtained greater attention in the last decades, researchers in the software engineering field are still used to place software and humans on two opposite sides. Nevertheless, the human factors involved in the software development process are vital to successfully completing a software project while increasing its quality and reducing its bugs. During this talk, I will present how different kinds of analysis can be used and adapted to explore and evaluate human factors during IoT software design and implementation.

[Slide07]

15:45-16:15. A Case-study: domain-specific languages and trusted communication in an IoT SmartCities scenario.
Corrado Santoro (Università degli Studi di Catania)

Abstract. The talk deals with a SmartCities scenario in which several IoT devices, spread over a town, cooperate to handle a traffic management application; in particular, we consider a set of devices able to monitor car traffic (by identifying bluetooth car equipment), and other devices that control traffic lights and smart traffic signals.

Apart from the specific aspects of the application itself, the case-study concentrates the attention on two main concerns.

The first one is related to the derivation and application of a DSL able to handle the requirements of the said scenario; for its implementation, rather than considering to write parsers and scanners, we aim to employ the PHIDIAS platform, a python-based tool that allows developers to implement BDI agents by means of a declarative and extensible language. PHIDIAS is also easily portable that it runs on both classical PC-based hardware and embedded boards by exploiting micropython, thus making it ready for IoT environments.

The second concern is related to communication. We aim at integrating trust information in communications between IoT devices. Feedbacks are used to calculate trustworthiness information (reputation) which are saved in the edge and/or in the cloud. We focus on two main aspects. First of all, we will study how different reputation models can help the IoT devices to perform better and to be effective in isolating malfunctioning or malicious devices. Secondly, we want to study how a reputation model can help IoT devices to form groups or clusters with similar characteristics of performance and high level of mutual trustworthiness. IoT devices in the same cluster can interact with each other in faster and secure way in order to accomplish complex tasks.

[Slide08]

16:15-16:45. Stream and River Monitoring: Evaluation of IoT languages and Prototype Development.
Alessio Ferrari (ISTI-CNR Pisa)

Abstract. Floods take the lives of more people than many other natural disasters, due to their frequent occurrence and unpredictable nature. Water-related events are common in northern-west Tuscany, an area in which soil instability and poorly maintained river banks concur in creating erosion phenomena and floods that impact rural areas. The combined use of IoT technologies such as ultrasonic sensors for water level monitoring, smart weather stations, drones equipped with cameras, etc., can enable continuous and remote supervision of rivers and streams, so that changes in the natural environment can be quickly identified. Designing and configuring these systems is particularly complex, as different contexts require different deployment strategies and possibly unexpected system configurations. Within T-LADIES, the PI unit will: 1) identify currently available languages for the development and configuration of IoT systems; 2) evaluate them with the involvement of relevant stakeholders; 3) will develop a prototype stream and river monitoring solution, in which the usage of different languages can be explored. The prototype can serve as a test bed to evaluate also the solutions from other partners of T-LADIES.

16:45-17:00. Questions and (Maybe) Answers, Discussion and Brainstorming.

17:00-17:30. Coffee Break.

17:30-17:45. Introduction to WP2: Interaction Mechanisms. [SlideWP2]
Maurice H. ter Beek (ISTI-CNR Pisa)

17:45-18:15. Specification, Synthesis and Implementation of Contract-based Applications via Contract Automata.
Davide Basile (ISTI—CNR Pisa)

Abstract. Behavioural contracts have been introduced in the literature to model the behaviour of ensembles of services in terms of their interactions. This allows to reason formally about well-behaving properties of ensembles of services, and to build applications that are verified by construction against these properties. Behavioural contracts modelled as Finite State Automata are dubbed contract automata. In this talk, I will present the contract automata formalism, its operations of composition and synthesis, and their extension to modalities and product lines. I will also introduce the Contract Automata Toolkit (CAT), currently providing a library implementing in Java contract automata and its operations, a graphical application to design contracts and a runtime environment to implement applications specified with contract automata.

[Slide10]

18:15-18:45. A Brief Introduction to Software Agents and Their Programming Languages.
Giuseppe Petrosino (Università degli Studi di Modena e Reggio Emilia)

Abstract. The initial part of this talk introduces software agents and their peculiarities in the landscape of distributed software systems. Then, a software framework to develop software agents in Java is briefly discussed to focus on the primary abstractions that it provides. Finally, an agent-oriented programming language specifically designed to develop software agents using the aforementioned framework is overviewed. The basic building blocks of the language are presented, and some plans for future developments are discussed.

[Slide11]

18:45-19:00. Questions and (Maybe) Answers, Discussion and Brainstorming.

20:00. Social Dinner at Alle Bandierine

Thursday, July 7, 2022

09:00-10:00. Modelling and Verification of Multi-Agent Systems. (Keynote)
Rocco De Nicola (IMT Lucca)

[Slide12]

10:00-10:30. Coffee Break.

10:30-10:45. Introduction to WP3: Advanced Type Systems. [SlideWP3]
Davide Ancona (Università degli Studi di Genova)

10:45-11:15. Coeffects for Java-like languages.
Riccardo Bianchini (Università degli Studi di Genova)

Abstract. Type-and-coeffect systems are enriched type systems which track program requirements on the context, namely, use of external resources, typically through annotations on single variables. The objective of our work is to investigate the use of coeffects to express properties of interest in Java-like languages. In particular, we propose a language design where, by relying on the inheritance mechanism of OO languages, coeffect annotations are expressions of the language itself, of (subclasses of) a predefined class Coeffect.

Joint work with Francesco Dagnino, Paola Giannini, Elena Zucca

[Slide13]

11:15-11:45. Global Types for Multiparty Sessions.
Paola Giannini (Università del Piemonte Orientale)

Abstract. Multiparty sessions (MPS) formalise message exchange protocols. Global types play the fundamental role of describing the whole scenario, while the behaviour of participants is implemented by processes. The agreement between global types and MPS has been classically based on defining projection of global types onto local types (session types) and a notion of agreement of local types with processes. If the projection is defined for all participants and each local type agrees with the participant's process the MPS enjoys the "progress property", i.e., all participants willing to communicate will be able to do it and, in case of asynchronous communication, also all sent messages will be received. Projection limits the expressiveness of global types, ruling out relevant protocols. In the talk I give a general introduction of the subject and present some recent work in the definition of more permissive global types and new techniques to enforce agreement between MPS and global types not relying on projection.

Joint work with Francesco Dagnino, Mariangiola Dezani and Ilaria Castellani

[Slide14]

11:45-12:00. Questions and (Maybe) Answers, Discussion and Brainstorming.

12:00-12:00. Resuming WP2: Interaction Mechanisms.
Maurice H. ter Beek (ISTI-CNR Pisa)

12:00-12:30. Incremental variability models for language composition inference
Luca Favalli (Università degli Studi di Milano)

Abstract. Following the language-oriented programming paradigm, domain-specific languages (DSL) have become a successful technique in the development of complex systems. However, DSLs—as most other programming languages—are usually implemented as monolithic interpreters and compilers, negating any reuse opportunity despite any commonalities different languages may share. In recent years, researchers and practitioners gained interest in product line engineering to improve the reusability of language assets and the management of variability-rich systems, introducing the notions of language workbenches and language product lines (LPLs). The challenge for language designers is to take advantage of the commonalities among any similar DSLs by reusing formerly defined language constructs. Despite the research efforts, managing the variability of DSLs is inherently complex and concerns three dimensions of variability—abstract syntax, concrete syntax and semantics—which can be properly and independently defined only if the language workbench supports the exogenous modularization technique. Modeling all the three dimensions of the variability space upfront and following a top-down approach may be error-prone; moreover, the resulting variability model and its implementation may be hard to maintain. Instead, we propose an approach in which the variability model of a LPL is developed incrementally. First, the model is extracted from the abstract syntax modules in a bottom-up fashion. Then, the semantics are inferred during the configuration process to suggest possible compositions and eventually to produce valid language specifications, with the support of pre-conditions and post-conditions over each semantic asset compatible with the language grammar. Upon completion, the configuration retroactively increments the variability model with the newly created language features and their dependencies.

Joint work with Walter Cazzola.

[Slide15]

12:39-13:00, Featured Team Automata.
Maurice H. ter Beek (ISTI-CNR Pisa)

Abstract. Team automata describe a network of automata with input and output actions, extended with synchronisation policies guiding how many input and output actions can synchronise. Given such a team automaton, one can reason over communication properties such as receptiveness (all sent messages must be received) and responsiveness (all pending receives must be satisfied). Featured team automata support variability in the development and analysis of teams by concisely describing a family of concrete product models for specific configurations determined by feature selection. The analysis of communication-safety properties in a product-wise manner quickly becomes impractical. Therefore, we lift the notions of receptiveness to the level of family models. We show that featured (weak) receptiveness of featured team automata characterises (weak) receptiveness for all product instantiations. So far we focused on identifying communication properties. However, verifying automatically these properties is non-trivial, as it may involve traversing a set of networks of interacting automata with a large state space. We are currently investigating (1) how to characterise communication properties for team automata (and its subsumed models) using test-free propositional dynamic logic, and (2) how to use this characterisation to verify communication properties using model checking. A prototypical tool supports the developed theory and interacts with mCRL2 for the model checking.

Joint work with Guillermina Cledou, Rolf Hennicker, and José Proença

[Slide16]

13:00-13:00. Closing.
Walter Cazzola (Università degli Studi di Milano)

13:00-14:00. Lunch.