@ARTICLE{Cazzola21b, author = {Cazzola, Walter and Favalli, Luca}, title = {{Towards a Recipe for Language Decomposition: Quality Assessment of Language Product Lines}}, journal = {{Empirical Software Engineering}}, publisher = {Springer}, year = 2022, volume = 27, number = {}, pages = {}, month = apr, url = {https://trebuchet.public.springernature.app/get_content/a573ab10-aec4-46dd-a4ba-77ce4a663722}, abstract = {Programming languages are complex systems that are usually implemented as monolithic interpreters and compilers. 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). Nonetheless, language development remains a complex activity and design or implementation flaws can easily waste the efforts of decomposing a language specification into language features. Poorly designed language decompositions result in high inter-dependent components, reducing the variability space of the LPL system and its maintainability. One should detect and fix the design flaws posthaste to prevent these risks while minimizing the development overhead. Therefore, various aspects of the quality of a language decomposition should be quantitatively measurable through adequate metrics. The evaluation, analysis and feedback of these measures should be a primary part of the engineering process of a LPL. In this paper, we present an exploratory study trying to capture these aspects by introducing a design methodology for LPLs; we define the properties of a good language decomposition and adapt a set of metrics from the literature to the framework of language workbenches. Moreover, we leverage the AiDE 2 LPL engineering environment to perform an empirical evaluation of 26 Neverlang-based LPLs based on this design methodology. Our contributions form the foundations of a design methodology for Neverlang-based LPLs. This methodology is comprised of four different elements: i)~an engineering process that defines the order in which decisions are made, ii)~an integrated development environment for LPL designers and iii)~some best practices in the design of well-structured language decomposition when using Neverlang, supported by iv)~a variety of LPL metrics that can be used to detect errors in design decisions.}, doi = {10.1007/s10664-021-10074-6}, note = {} } @ARTICLE{Cazzola22, author = {Bertolotti, Francesco and Cazzola, Walter}, title = {{Fold2Vec: Towards a Statement Based Representation of Code for Code Comprehension}}, journal = {{Transaction on Software Engineering and Methodology}}, publisher = {ACM}, year = 2023, volume = 32, number = 1, pages = {6:1--6:31}, month = feb, pubtype = {journal}, url = {https://dl.acm.org/doi/pdf/10.1145/3514232}, abstract = {We introduce a novel approach to source code representation to be used in combination with neural networks. Such a representation is designed to permit the production of a continuous vector for each code statement. In particular, we present how the representation is produced in the case of Java source code. We test our representation for three tasks: code summarization, statement separation, and code search. We compare with the state-of-the-art non-autoregressive and end-to-end models for these tasks. We conclude that all tasks benefit from the proposed representation to boost their performance in terms of f1-score, accuracy, and MRR, respectively. Moreover, we show how models trained on code summarization and models trained on statement separation can be combined to address methods with tangled responsibilities. Meaning that these models can be used to detect code misconduct.}, doi = {10.1145/3514232}, note = {} } @ARTICLE{Cazzola22b, author = {Cazzola, Walter and Cesarini, Francesco and Tansini, Luca}, title = {{PerformERL: A Performance Testing Framework for Erlang}}, journal = {Distributed Computing}, publisher = {Springer}, year = 2022, volume = 35, number = {}, pages = {439--454}, month = may, url = {https://link.springer.com/content/pdf/10.1007/s00446-022-00429-7.pdf}, abstract = {The Erlang programming language is used to build concurrent, distributed, scalable and resilient systems. Every component of these systems has to be thoroughly tested not only for correctness, but also for performance. Performance analysis tools in the Erlang ecosystem, however, do not provide a sufficient level of automation and insight needed to be integrated in modern tool chains. In this paper, we present PerformERL: an extendable performance testing framework that combines the repeatability of load testing tools with the details on how the resources are internally used typical of the performance monitoring tools. These features allow PerformERL to be integrated in the early stages of testing pipelines, providing users with a systematic approach to identifying performance issues. This paper introduces the PerformERL framework, focusing on its features, design and imposed monitoring overhead measured through both theoretical estimates and trial runs on systems in production. The uniqueness of the features offered by PerformERL, together with its usability and contained overhead prove that the framework can be avaluable resource in the development and maintenance of Erlang applications.}, doi = {10.1007/s00446-022-00429-7}, note = {} } @INPROCEEDINGS{Cazzola22c, author = {Bertolotti, Francesco and Cazzola, Walter and Favalli, Luca}, title = {{Features, Believe It or Not! A Design Pattern for First-Class Citizen Features on Stock JVM}}, booktitle = {{Proceedings of the 26th International Software Product Line Conference (SPLC'22)}}, year = 2022, editor = {Cleland-Huang, Jane and Assun\c{c}\~ao, Wesley K. G.}, pages = {32--42}, address = {Graz, Austria}, organization = {}, publisher = {ACM}, volume = {}, number = {}, series = {}, month = sep, url = {https://dl.acm.org/doi/abs/10.1145/3546932.3546989}, abstract = {Modern software systems must fulfill the needs of an ever-growing customer base. Due to the innate diversity of human needs, software should be highly customizable and reconfigurable. Researchers and practitioners gained interest in software product lines (SPL), mimicking aspects of product lines in industrial production for the engineering of highly-variable systems. There are two main approaches towards the engineering of SPLs. The first uses macros---such as the \texttt{\#ifdef} macro in C. The second---called feature-oriented programming (FOP)---uses variability-aware preprocessors called composers to generate a program variant from a set of features and a configuration. Both approaches have disadvantages. Most notably, these approaches are usually not supported by the base language; for instance Java is one of the most commonly used FOP languages among researchers, but it does not support macros rather it relies on the C preprocessor or a custom one to translate macros into actual Java code. As a result, developers must struggle to keep up with the evolution of the base language, hindering the general applicability of SPL engineering. Moreover, to effectively evolve a software configuration and its features, their location must be known. The problem of recording and maintaining traceability information is considered expensive and error-prone and it is once again handled externally through dedicated modeling languages and tools. Instead, to properly convey the FOP paradigm, software features should be treated as first-class citizens using concepts that are proper to the host language, so that the variability can be expressed and analyzed with the same tools used to develop any other software in the same language. In this paper, we present a simple and flexible design pattern for JVM-based languages---dubbed devise pattern---that can be used to express feature dependencies and behaviors with a light-weight syntax both at domain analysis and at domain implementation level. To showcase the qualities and feasibility of our approach, we present several variability-aware implementations of a MNIST-encoder---including one using the devise pattern---and compare strengths and weaknesses of each approach. }, doi = {10.1145/3546932.3546989}, note = {} } @InProceedings{CicconeDP22, author = {Ciccone, Luca and Dagnino, Francesco and Padovani, Luca}, title = {{Fair Termination of Multiparty Sessions}}, booktitle = {36th European Conference on Object-Oriented Programming (ECOOP 2022)}, pages = {26:1--26:26}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, year = {2022}, volume = {222}, editor = {Ali, Karim and Vitek, Jan}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, url = {https://drops.dagstuhl.de/opus/volltexte/2022/16254}, doi = {10.4230/LIPIcs.ECOOP.2022.26}, abstract = { There exists a broad family of multiparty sessions in which the progress of one session participant is not unconditional, but depends on the choices performed by other participants. These sessions fall outside the scope of currently available session type systems that guarantee progress. In this work we propose the first type system ensuring that well-typed multiparty sessions, including those exhibiting the aforementioned dependencies, fairly terminate. Fair termination is termination under a fairness assumption that disregards those interactions deemed unfair and therefore unrealistic. Fair termination, combined with the usual safety properties ensured within sessions, not only is desirable per se, but it entails progress and enables a compositional form of static analysis such that the well-typed composition of fairly terminating sessions results in a fairly terminating program. }, note = {} } @InProceedings{DagninoG22, author = {Dagnino, Francesco and Gavazzo, Francesco}, title = {{A Fibrational Tale of Operational Logical Relations}}, booktitle = {7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022)}, pages = {3:1--3:21}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, year = {2022}, volume = {228}, editor = {Felty, Amy P.}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, url = {https://drops.dagstuhl.de/opus/volltexte/2022/16284}, doi = {10.4230/LIPIcs.FSCD.2022.3}, abstract = {Logical relations built on top of an operational semantics are one of the most successful proof methods in programming language semantics. In recent years, more and more expressive notions of operationally-based logical relations have been designed and applied to specific families of languages. However, a unifying abstract framework for operationally-based logical relations is still missing. We show how fibrations can provide a uniform treatment of operational logical relations, using as reference example a Ī»-calculus with generic effects endowed with a novel, abstract operational semantics defined on a large class of categories. Moreover, this abstract perspective allows us to give a solid mathematical ground also to differential logical relations - a recently introduced notion of higher-order distance between programs - both pure and effectful, bringing them back to a common picture with traditional ones.}, note = {} } @inproceedings{DagninoP22, author = {Dagnino, Francesco and Pasquali, Fabio}, title = {Logical Foundations of Quantitative Equality}, booktitle = {Proceedings of the 37th Annual ACM/IEEE Symposium on Logic in Computer Science}, location = {Haifa, Israel}, series = {LICS '22}, articleno = {16}, numpages = {13}, year = {2022}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3531130.3533337}, doi = {10.1145/3531130.3533337}, abstract = {In quantitative reasoning one compares objects by distances, instead of equivalence relations, so that one can measure how much they are similar, rather than just saying whether they are equivalent or not. In this paper we aim at providing a logical ground to quantitative reasoning with distances in Linear Logic, using the categorical language of Lawvereā€™s doctrines. The key idea is to see distances as equality predicates in Linear Logic. We use graded modalities to write a resource sensitive substitution rule for equality, which allows us to give it a quantitative meaning by distances. We introduce a deductive calculus for (Graded) Linear Logic with quantitative equality and the notion of Lipschitz doctrine to give it a sound and complete categorical semantics. We also describe a universal construction of Lipschitz doctrines, which generates examples based for instance on metric spaces and quantitative realisability.}, keywords = {graded modalities, linear logic, hyperdoctrines, quantitative reasoning}, } @inproceedings{AnconaBarbieriZuccaFLOPS22, author = {Davide Ancona and Pietro Barbieri and Elena Zucca}, title = {Enhancing Expressivity of Checked Corecursive Streams}, booktitle = {Functional and Logic Programming - 16th International Symposium, {FLOPS} 2022, Kyoto, Japan, May 10-12, 2022, Proceedings}, pages = {1--18}, year = {2022}, doi = {10.1007/978-3-030-99461-7\_1}, editor = {Michael Hanus and Atsushi Igarashi}, series = {Lecture Notes in Computer Science}, volume = {13215}, publisher = {Springer}, abstract = {We propose a novel approach to stream definition and manipulation. Our solution is based on two key ideas. Regular corecursion, which avoids non termination by detecting cyclic calls, is enhanced, by allowing in equations defining streams other operators besides the stream constructor. In this way, some non-regular streams are definable. Furthermore, execution includes a runtime check to ensure that the stream generated by a function call is well-defined, in the sense that access to an arbitrary index always succeeds. We extend the technique beyond the simple stream operators considered in previous work, notably by adding an interleaving combinator which has a non-trivial recursion scheme.}, } @inproceedings{AnconaBarbieriZuccaICTCS22, author = {Davide Ancona and Pietro Barbieri and Elena Zucca}, title = {Equality of corecursive streams defined by finitary equational systems}, booktitle = {{ICTCS22} Proceedings}, year = {2022}, publisher = {CEUR}, abstract = {In recent work, non-regular streams have been defined corecursively, by representing them with finitary equational systems built on top of various operators, besides the standard constructor. With finitary equational systems based only on the stream constructor, one can use the free theory of regular (a.k.a. rational) trees to get a sound and complete procedure to decide whether two streams are equal. However, this is not the case if one allows other operators in equations, since the underlying equational theory becomes non-trivial, hence equality of regular trees is too strong to guarantee termination of corecursive functions defined even only with the constructor and tail operators. To overcome this problem, we provide a weaker definition of equality between streams denoted by finitary equational systems built on different stream operators, including tail operator and constructor, and prove its soundness. }, note ={To appear} } @inproceedings{EgidiGianniniVenturaICSOFT22, author = {Lavinia Egidi and Paola Giannini and Lorenzo Ventura}, editor = {Hans{-}Georg Fill and Marten van Sinderen and Leszek A. Maciaszek}, title = {Multiparty-session-types Coordination for Core Erlang}, booktitle = {Proceedings of the 17th International Conference on Software Technologies, {ICSOFT} 2022}, pages = {532--541}, publisher = {{SCITEPRESS}}, year = {2022}, url = {https://doi.org/10.5220/0011316600003266}, doi = {10.5220/0011316600003266}, abstract = {In this paper, we present a formalization of multiparty-session-type coordination for a core subset of Erlang and provide a tool for checking the correctness of a system against the specification of its protocol. In Erlang "actors" are primitive entities, which communicate only through explicit "asynchronous message passing". Our tool ensures that if an Erlang system is well typed, then it does not incur in deadlocks or have actors getting stuck waiting for messages that never arrive; moreover any message that is sent will eventually be read. The tool is based on "multiparty session types", a formalism introduced to specify the structure of interactions and to ensure safety properties. }, } @ARTICLE{BDLMPS22, author = {ter Beek, Maurice H. and Damiani, Ferruccio and Lienhardt, Michael and Mazzanti, Franco and Paolini, Luca and Scarso, Giordano}, title = {{{FTS4VMC}: a Front-End Tool for Static Analysis and Family-Based Model Checking of {FTSs} with {VMC}}}, journal = {{Science of Computer Programming}}, publisher = {}, year = 2022, volume = 224, number = {}, pages = {}, month = {}, note = {}, doi = {10.1016/j.scico.2022.102879}, abstract = {FTS4VMC is a publicly available front-end tool for the static analysis and family-based model checking of a Featured Transition System (FTS). It can detect ambiguities in an FTS, disambiguate an ambiguous FTS, transform an FTS into a Modal Transition System (MTS), and interact with the VMC model checker for family-based verification} } @ARTICLE{BF22, author = {ter Beek, Maurice H. and Ferrari, Alessio}, title = {{Empirical Formal Methods: {G}uidelines for Performing Empirical Studies on Formal Methods}}, journal = {{Software}}, publisher = {}, year = 2022, volume = 1, number = 4, pages = {381--416}, month = {}, note = {}, doi = {10.3390/software1040017}, abstract = {Empirical studies on formal methods and tools are rare. In this paper, we provide guidelines for such studies. We mention their main ingredients and then define nine different study strategies (usability testing, laboratory experiments with software and human subjects, case studies, qualitative studies, surveys, judgement studies, systematic literature reviews, and systematic mapping studies) and discuss for each of them their crucial characteristics, the difficulties of applying them to formal methods and tools, typical threats to validity, their maturity in formal methods, pointers to external guidelines, and pointers to studies in other fields. We conclude with a number of challenges for empirical formal methods.} } @ARTICLE{BBLCL22, author = {Basile, Davide and ter Beek Maurice H. and Lazreg, Sami and Cordy, Maxime and Legay, Axel}, title = {{Static Detection of Equivalent Mutants in Real-Time Model-Based Mutation Testing: {A}n Empirical Evaluation}}, journal = {{Empirical Software Engineering}}, publisher = {}, year = 2022, volume = 27, number = 7, pages = {160:1--160:55}, month = {}, note = {}, doi = {10.1007/s10664-022-10149-y}, abstract = {Model-based mutation testing has the potential to effectively drive test generation to reveal faults in software systems. However, it faces a typical efficiency issue since it could produce many mutants that are equivalent to the original system model, making it impossible to generate test cases from them. We consider this problem when model-based mutation testing is applied to real-time system product lines, represented as timed automata. We define novel, time-specific mutation operators and formulate the equivalent mutant problem in the frame of timed refinement relations. Further, we study in which cases a mutation yields an equivalent mutant. Our theoretical results provide guidance to system engineers, allowing them to eliminate mutations from which no test case can be produced. Our empirical evaluation, based on a proof-of-concept implementation and a set of benchmarks from the literature, confirms the validity of our theory and demonstrates that in general our approach can avoid the generation of a significant amount of the equivalent mutants.} } @ARTICLE{Cazzola22d, author = {Cazzola, Walter and Favalli, Luca}, title = {{The Language Mutation Problem: Leveraging Language Product Lines for Mutation Testing of Interpreters}}, journal = {{Journal of Systems and Software}}, publisher = {Elsevier}, year = 2023, volume = 195, number = {}, pages = {}, month = oct, abstract = {Compilers translate programs from a high level of abstraction into a low level representation that can be understood and executed by the computer; interpreters directly execute instructions from source code to convey their semantics. Undoubtedly, the correctness of both compilers and interpreters is fundamental to reliably execute the semantics of any software developed by means of high-level languages. Testing is one of the most important methods to detect errors in any software, including compilers and interpreters. Among testing methods, mutation testing is an empirically effective technique often used to evaluate and improve the quality of test suites. However, mutation testing imposes severe demands in computing resources due to the large number of mutants that need to be generated, compiled and executed. In this work, we introduce a mutation approach for programming languages that mitigates this problem by leveraging the properties of language product lines, language workbenches and separate compilations. In this approach, the base language is taken as a black-box and mutated by means of mutation operators performed at language feature level to create a family of mutants of the base language. Each variant of the mutant family is created at runtime, without any access to the source code and without performing any additional compilation. We report results from a preliminary case study in which mutants of an \textsf{ECMAScript} interpreter are tested against the \textsf{Sputnik} conformance test suite for the \textsf{ECMA-262} specification. The experimental data indicates that this approach can be used to create generally non-trivial mutants.}, doi = {10.1016/j.jss.2022.111533}, note = {} } @article{CastellaniDCG23, title = {Event structure semantics for multiparty sessions}, journal = {Journal of Logical and Algebraic Methods in Programming}, volume = {131}, pages = {100844}, year = {2023}, issn = {2352-2208}, doi = {https://doi.org/10.1016/j.jlamp.2022.100844}, url = {https://www.sciencedirect.com/science/article/pii/S2352220822000979}, author = {Ilaria Castellani and Mariangiola Dezani-Ciancaglini and Paola Giannini}, keywords = {Communication-centric systems, Communication-based programming, Process calculi, Event structures, Multiparty session types}, abstract = {We propose an interpretation of multiparty sessions as Flow Event Structures, which allows concurrency within sessions to be explicitly represented. We show that this interpretation is equivalent, when the multiparty sessions can be described by global types, to an interpretation of such global types as Prime Event Structures.} } @ARTICLE{BBBF22, author = {Davide Basile and Maurice H. ter Beek and Giovanna Broccia and Alessio Ferrari}, title = {{Empirical Software Engineering and Formal Methods for IoT Systems}}, journal = {{ERCIM News}}, publisher = {}, year = 2022, volume = 131, number = {}, pages = {34--35}, month = {}, url = {https://ercim-news.ercim.eu/en131/r-i/empirical-software-engineering-and-formal-methods-for-iot-systems}, note = {}, abstract = {Researchers from the Formal Methods and Tools (FMT) lab of ISTI--CNR are working on the application of formal methods to devise interaction protocols for safe-by-construction IoT Systems of Systems. They are also working on the empirical investigation and evaluation of the effectiveness of techniques and methodologies proposed for IoT application scenarios. The research is being conducted in the context of the national project T-LADIES, funded by the Italian Ministry of Education, University and Research (MIUR) under the program for Projects of National Interest (PRIN)} } @article{BianchiniDGZS22, author = {Bianchini, Riccardo and Dagnino, Francesco and Giannini, Paola and Zucca, Elena and Servetto, Marco}, title = {Coeffects for Sharing and Mutation}, year = {2022}, issue_date = {October 2022}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, volume = {6}, number = {OOPSLA2}, doi = {10.1145/3563319}, abstract = {In type-and-coeffect systems, contexts are enriched by coeffects modeling how they are actually used, typically through annotations on single variables. Coeffects are computed bottom-up, combining, for each term, the coeffects of its subterms, through a fixed set of algebraic operators. We show that this principled approach can be adopted to track sharing in the imperative paradigm, that is, links among variables possibly introduced by the execution. This provides a significant example of non-structural coeffects, which cannot be computed by-variable, since the way a given variable is used can affect the coeffects of other variables. To illustrate the effectiveness of the approach, we enhance the type system tracking sharing to model a sophisticated set of features related to uniqueness and immutability. Thanks to the coeffect-based approach, we can express such features in a simple way and prove related properties with standard techniques.}, journal = {Proc. ACM Program. Lang.}, month = {oct}, articleno = {156}, numpages = {29}, keywords = {sharing, Java, coeffect systems} } @article{DagninoGD23, author = {Francesco Dagnino and Paola Giannini and Mariangiola Dezani{-}Ciancaglini}, title = {Deconfined Global Types for Asynchronous Sessions}, journal = {Logical Methods in Computer Science}, volume = {19}, number = {1}, year = {2023}, doi = {10.46298/lmcs-19(1:3)2023}, } @article{BianchiniD23, author = {Riccardo Bianchini and Francesco Dagnino}, title = {Query{AGT}: Asynchronous global types in co-logic programming}, journal = {Science of Computer Programming}, volume = {225}, pages = {102895}, year = {2023}, publisher = {Elsevier}, doi = {10.1016/j.scico.2022.102895}, } @INPROCEEDINGS{Cazzola23, author = {Broccia, Giovanna and Ferrari, Alessio and ter Beek, Maurice and Cazzola, Walter and Favalli, Luca and Bertolotti, Francesco}, title = {{Evaluating a Language Workbench: from Working Memory Capacity to Comprehension to Acceptance}}, booktitle = {{Proceedings of the 31st International Conference on Program Comprehension (ICPC'23)}}, year = 2023, OPTeditor = {Catolino, Gemma and De Roover, Coen}, pages = {}, OPTaddress = {Melbourne, Australia}, organization = {}, publisher = {ACM}, volume = {}, number = {}, series = {}, OPTmonth = may, OPTpubtype = {conference}, url = {}, new = {}, OPTkeywords = {dsl}, abstract = {Language workbenches are tools that enable the definition, reuse and composition of programming languages and their ecosystem. This breed of frameworks aims to make the development of new languages easier and more affordable. Consequently, the understandability and learnability of the language used in a language workbench (i.e., the meta-language) should be an important aspect to consider and evaluate. To the best of our knowledge, although the quantitative aspects of language workbenches are often discussed in the literature, the evaluation of understandability and learnability are typically neglected. Neverlang is a language workbench that enables the definition of languages with a modular approach. This paper presents a preliminary study that intends to assess the comprehensibility of Neverlang programs, evaluated in terms of users' ffectiveness and efficiency in a code comprehension task. The study also investigates the relationship between Neverlang comprehensibility and the users' working memory capacity. Furthermore, we intend to capture the relationship between Neverlang comprehensibility and users' acceptance, in terms of perceived ease of use, perceived usefulness, and intention to use. Our preliminary results on 10 subjects suggest that the users' working memory capacity may be related to the ability to comprehend Neverlang programs. On the other hand, effectiveness and efficiency do not appear to be associated with an increase in users' acceptance variables.}, note = {} } @ARTICLE{Cazzola23b, author = {Bertolotti, Francesco and Cazzola, Walter and Favalli, Luca}, title = {{On the Granularity of Linguistic Reuse}}, journal = {{Journal of Systems and Software}}, publisher = {Elsevier}, year = 2023, volume = 202, number = {}, pages = {}, month = aug, pubtype = {journal}, url = {}, new = {}, keywords = {dsl modularity sw-engineering}, abstract = {Programming languages are complex software systems integrated across an ecosystem of different applications such as language compilers or interpreters but also an integrated development environment comprehensive of syntax highlighting, code completion, error recovery, and a debugger. The complexity of language ecosystems can be faced using language workbenches---i.e., tools that tackle the development of programming languages, domain specific languages and their ecosystems in a modular way. As with any other software system, one of the priorities that developers struggle to achieve when developing programming languages is reusability. After all, the capacity to easily reuse and adapt existing components to new scenarios can dramatically improve development times. Therefore, as programming languages offer features to reuse existing code, language workbenches should offer tools to reuse existing language assets. However, reusability can be achieved in many different ways. In this work, we identify six forms of linguistic reusability, ordered by level of granularity: (i)~sub-languages composition, (ii)~language features composition, (iii)~syntax and semantics assets composition, (iv)~semantic assets composition, (v)~actions composition, and (vi)~action extension. We use these mechanisms to extend the taxonomy of language composition proposed by Erdweg et al. To show a concrete application of this taxonomy, we evaluate the capabilities provided by the Neverlang language workbench with regards to our taxonomy and extend it by adding explicit support for any granularity level that was originally not supported. This is done by instantiating two levels of reusability as actual operators---desugaring, and delegation. We evaluate these operators against the clone-and-own approach, which was the only form of reuse at that level of granularity prior to the introduction of explicit operators. We show that with the clone-and-own approach the design quality of the source code is negatively affected. We conclude that language workbenches can benefit from the introduction of mechanisms to explicitly support reuse at all granularity levels.}, doi = {10.1016/j.jss.2023.111704}, note = {} } @ARTICLE{Cazzola23c, author = {Cazzola, Walter and Favalli, Luca}, title = {{Scrambled Features for Breakfast: Concept, and Practice of Agile Language Development}}, journal = {{Communications of the ACM}}, publisher = {ACM}, year = 2023, volume = 66, number = 11, pages = {30--40}, month = nov, pubtype = {journal}, url = {}, new = {}, keywords = {dsl modularity sw-engineering}, abstract = {Modular software development is taken for granted thanks to the abstractions of modern programming languages. However, the programming languages themselves are still often developed as a monolithic whole, despite them being the very foundation our software is based on. Mainstream programming languages are rarely developed incrementally and their evolution and maintenance are a mere afterthought. The growing research field of language workbenches tries to improve language design and development by employing modularization techniques that maximize code reuse up to the language construct granularity. In this paper, we investigate how such an approach fits an agile style of development: agile engineering concepts such as product backlog items and sprint goals can be directly mapped onto language workbench concepts such as language features and language variants. This direct mapping allows for an easier development of modular, extensible and maintainable programming languages. We conceptualized an agile language development style that acknowledges such a mapping and then turned concepts into theory by outlining an agile language development methodology. Then, thanks to our partnership with Tyl, we put theory into practice in an industrial production environment. Now, we share our experience on the agile creation process of a domain-specific language for the enterprise resource planning (ERP).}, doi = {10.1145/3596217}, note = {} } @INPROCEEDINGS{Basile23fse, author = {Basile, Davide and ter Beek, Maurice H. and G\"ottmann, Hendrik and Lochau, Malte}, title = {{Mutant Equivalence as Monotonicity in Parametric Timed Games}}, booktitle = {{Proceedings of the 11th International Conference on Formal Methods in Software Engineering (FormaliSE'23)}}, year = 2023, editor = {}, pages = {}, OPTaddress = {Melbourne, Australia}, organization = {}, publisher = {IEEE}, volume = {}, number = {}, series = {}, OPTmonth = may, note = {}, abstract = {The detection of faults in software systems can be enhanced effectively by model-based mutation testing. The efficiency of this technique is hindered when mutants are equivalent to the original system model, since this makes them useless. Recently, the application of model-based mutation testing to realtime systems modelled as timed games has been investigated, which has resulted in guidelines for statically avoiding equivalent mutants. In this paper, we recast this problem into the framework of parametric timed games. We then prove a correspondence between theoretical results for the detection of equivalent mutants in timed games and the property of monotonicity that is known to hold for a sub-class of parametric timed games called L/U parametric timed games. The presented results not only simplify the theory underlying the detection of equivalent mutants in timed games, but at the same time they improve the expressiveness of a known decidable fragment of parametric timed games for which monotonicity holds.} } @INPROCEEDINGS{BCHP23, author = {Maurice H. ter Beek and Guillermina Cledou and Rolf Hennicker and Jos\'e Proen\c{c}a}, title = {{Can We Communicate? {U}sing Dynamic Logic to Verify Team Automata}}, booktitle = {{Proceedings of the 25th International Symposium on Formal Methods (FM'23)}}, year = 2023, editor = {Marsha Chechik and Joost-Pieter Katoen and Martin Leucker}, pages = {122--141}, address = {}, organization = {}, publisher = {Springer}, volume = {14000}, number = {}, series = {Lecture Notes in Computer Science}, month = {}, doi = {10.1007/978-3-031-27481-7_9}, note = {}, abstract = {Team automata describe networks of automata with input and output actions, extended with synchronisation policies guiding how many interacting components can synchronise on a shared input/output action. Given such a team automaton, we can reason over communication properties such as receptiveness (sent messages must be received) and responsiveness (pending receives must be satisfied). Previous work focused on how to identify these communication properties. However, automatically verifying these properties is non-trivial, as it may involve traversing networks of interacting automata with large state spaces. This paper investigates (1)~how to characterise communication properties for team automata (and subsumed models) using test-free propositional dynamic logic, and (2)~how to use this characterisation to verify communication properties by model checking. A prototype tool supports the theory, using a transformation to interact with the mCRL2 tool for model checking.} } @INPROCEEDINGS{BB23b, author = {Basile, Davide and ter Beek, Maurice H.}, title = {{Research Challenges in Orchestration Synthesis}}, booktitle = {{Proceedings of the 16th Interaction and Concurrency Experience (ICE'23)}}, year = 2023, editor = {Aubert, Cl\'ement and Di Giusto, Cinzia and Fowler, Simon and Safina, Larisa}, pages = {73--90}, address = {}, organization = {}, publisher = {}, volume = {383}, number = {}, series = {EPTCS}, month = {}, doi = {10.4204/EPTCS.383.5}, note = {}, abstract = {Contract automata allow to formally define the behaviour of service contracts in terms of service offers and requests, some of which are moreover optional and some of which are necessary. A composition of contracts is said to be in agreement if all service requests are matched by corresponding offers. Whenever a composition of contracts is not in agreement, it can be refined to reach an agreement using the orchestration synthesis algorithm. This algorithm is a variant of the synthesis algorithm used in supervisory control theory and it is based on the fact that optional transitions are controllable, whereas necessary transitions are at most semi-controllable and cannot always be controlled. In fact, the resulting orchestration is such that as much of the behaviour in agreement is maintained. In this paper, we discuss recent developments of the orchestration synthesis algorithm for contract automata. Notably, we present a refined notion of semi-controllability and compare it with the original notion by means of examples. We then discuss the current limits of the orchestration synthesis algorithm and identify a number of research challenges together with a research roadmap.} } @INPROCEEDINGS{BB23, author = {Basile, Davide and Maurice H. ter Beek}, title = {{A Runtime Environment for Contract Automata}}, booktitle = {{Proceedings of the 25th International Symposium on Formal Methods (FM'23)}}, year = 2023, editor = {Marsha Chechik and Joost-Pieter Katoen and Martin Leucker}, pages = {550--567}, address = {}, organization = {}, publisher = {Springer}, volume = {14000}, number = {}, series = {Lecture Notes in Computer Science}, month = {}, doi = {10.1007/978-3-031-27481-7_31}, note = {}, abstract = {Contract automata have been introduced for specifying applications through behavioural contracts and for synthesising their orchestrations as finite state automata. This paper addresses the realisation of applications from contract automata specifications. We present CARE, a new runtime environment to coordinate services implementing contracts that guarantees the adherence of the implementation to its contract. We discuss how CARE can be adopted to realise contract-based applications, its formal guarantees, and we identify the responsibilities of the involved business actors. Experiments show the benefits of adopting CARE with respect to manual implementations} } @article{BianchiniDGZ23tcs, author = {Riccardo Bianchini and Francesco Dagnino and Paola Giannini and Elena Zucca}, title = {A Java-like calculus with heterogeneous coeffects}, journal = {Theor. Comput. Sci.}, volume = {971}, pages = {114063}, year = {2023}, doi = {10.1016/j.tcs.2023.114063}, } @inproceedings{BianchiniDGZ23ecoop, author = {Riccardo Bianchini and Francesco Dagnino and Paola Giannini and Elena Zucca}, editor = {Karim Ali and Guido Salvaneschi}, title = {Multi-Graded Featherweight Java}, booktitle = {37th European Conference on Object-Oriented Programming, {ECOOP} 2023, July 17-21, 2023, Seattle, Washington, United States}, series = {LIPIcs}, volume = {263}, pages = {3:1--3:27}, publisher = {Schloss Dagstuhl - Leibniz-Zentrum f{\"{u}}r Informatik}, year = {2023}, doi = {10.4230/LIPIcs.ECOOP.2023.3}, } @article{fortino2023using, title={Using Trust Measures to Optimize Neighbor Selection for Smart Blockchain Networks in the IoT}, author={Fortino, Giancarlo and Messina, Fabrizio and Rosaci, Domenico and Sarn{\`e}, Giuseppe ML}, journal={IEEE Internet of Things Journal}, year={2023}, publisher={IEEE} } @article{fortino2022social, title={A Social Edge-Based IoT Framework Using Reputation-Based Clustering for Enhancing Competitiveness}, author={Fortino, Giancarlo and Fotia, Lidia and Messina, Fabrizio and Rosaci, Domenico and Sarn{\`e}, Giuseppe ML}, journal={IEEE Transactions on Computational Social Systems}, year={2022}, publisher={IEEE} } @ARTICLE{Cazzola23d, author = {Bertolotti, Francesco and Cazzola, Walter and Favalli, Luca}, title = {{\splps: Software Product Lines Extraction Driven by Language Server Protocol}}, journal = {{Journal of Systems and Software}}, publisher = {Elsevier}, year = 2023, volume = 205, number = {}, pages = {}, month = nov, pubtype = {journal}, url = {}, new = {}, cc = {}, keywords = {lpl dsl}, abstract = {Software product lines (SPL) describe highly-variable software systems as a family of similar products that differ in terms of the features they provide. The promise of SPL engineering is to enable massive software reuse by allowing software features to be reused across a variety of different products made for several customers. However, there are some disadvantages in the extraction of SPLs from standard applications. Most notably, approaches to the development of SPLs are not supported by the base language and use a syntax and composition techniques that require a deep understanding of the tools being used. Therefore, the same features cannot be used in a different application and developers must face a steep learning curve when developing SPLs for the first time or when switching from one approach to a different one. Ultimately, this problem is due to a lack of standards in the area of SPL engineering and in the way SPLs are extracted from variability-unaware applications. In this work, we present a framework based on LSP and dubbed SPLL PS that aims at standardizing such a process by decoupling the refactoring operations made by the user from the effect they have on the source code. This way, the server for a specific SPL development approach can be used across several development environments that provide clients with customized refactoring options. Conversely, the developers can use the same client to refactor SPLs made according to different approaches without needing to learn the syntax of each approach. To showcase the applicability of the approach, we present an evaluation performed by refactoring four SPLs according to two different approaches: the results show that a minimal implementation of the SPLL PS client and server applications can be used to reduce the effort of extracting an SPL up to the 93% and that it can greatly reduce or even completely hide the implementation details from the developer, depending on the chosen approach.}, doi = {10.1016/j.jss.2023.111809}, note = {} } @ARTICLE{Cazzola23e, author = {Bertolotti, Francesco and Cazzola, Walter}, title = {{CombTransformers: Statement-Wise Transformers for Statement-Wise Representations}}, journal = {{IEEE Transactions on Software Engineering}}, publisher = {IEEE}, year = 2023, volume = 49, number = 10, pages = {}, month = aug, pubtype = {journal}, url = {}, new = {}, cc = {}, keywords = {ml}, abstract = {This study presents a novel category of Transformer architectures known as comb transformers, which effectively reduce the space complexity of the self-attention layer from a quadratic to a sub-quadratic level. This is achieved by processing sequence segments independently and incorporating X -word embeddings to merge cross-segment information. The reduction in attention memory requirements enables the deployment of deeper architectures, potentially leading to more competitive outcomes. Furthermore, we design an abstract syntax tree (AST)-based code representation to effectively exploit comb transformer properties. To explore the potential of our approach, we develop nine specific instances based on three popular architectural concepts: funnel, hourglass, and encoder-decoder. These architectures are subsequently trained on three code-related tasks: method name generation, code search, and code summarization. These tasks encompass a range of capabilities: short/long sequence generation and classification. In addition to the proposed comb transformers, we also evaluate several baseline architectures for comparative analysis. Our findings demonstrate that the comb transformers match the performance of the baselines and frequently perform better.}, doi = {10.1109/TSE.2023.3310793}, note = {} } @INPROCEEDINGS{Cazzola23f, author = {Cazzola, Walter and Favalli, Luca}, title = {{Exceptions All Over the Shop: Modular, Customizable, Language-Indipendent Exception Handling Layer}}, booktitle = {{Proceedings of the 16th International Conference on Software Language Engineering (SLE'23)}}, year = 2023, editor = {Degueuele, Thomas and Scott, Elizabeth}, pages = {15--28}, address = {Cascais, Portugal}, organization = {}, publisher = {ACM}, volume = {}, number = {}, series = {}, month = oct, pubtype = {conference}, url = {}, new = {}, keywords = {dsl}, abstract = {The introduction of better abstractions is at the forefront of research and practice. Among many approaches, domain-specific languages are subject to an increase in popularity due to the need for easier, faster and more reliable application development that involves programmers and domain experts alike. To smooth the adoption of such a language-driven development process, researchers must create new engineering techniques for the development of programming languages and their ecosystems. Traditionally, programming languages are implemented from scratch and in a monolithic way. Conversely, modular and reusable language development solutions would improve maintainability, reusability and extensibility. Many programming languages share similarities that can be leveraged to reuse the same language feature implementations across several programming languages; recent language workbenches strive to achieve this goal by solving the language composition and language extension problems. Yet, some features are inherently complex and affect the behavior of several language features. Most notably, the exception handling mechanism involves varied aspects, such as the memory layout, variables, their scope, up to the execution of each statement that may cause an exceptional eventā€”e.g., a division by zero. In this paper, we propose an approach to untangle the exception handling mechanism dubbed the exception handling layer: its components are modular and fully independent from one another, as well as from other language features. The exception handling layer is language-independent, customizable with regards to the memory layout and supports unconventional exception handling language features. To avoid any assumptions with regards to the host language, the exception handling layer is a stand-alone framework, decoupled from the exception handling mechanism offered by the back-end. Then, we present a full-fledged, generic Java implementation of the exception handling layer. The applicability of this approach is presented through a language evolution scenario based on a Neverlang implementation of JavaScript and LogLang, that we extend with conventional and unconventional exception handling language features using the exception handling layer, with limited impact on their original implementation.}, doi = {10.1145/3623476.3623513}, note = {} } @INPROCEEDINGS{BHP23, author = {ter Beek, Maurice H. and Hennicker, Rolf and Proen\c{c}a, Jos\'e}, title = {{Realisability of Gobal Models of Interaction}}, booktitle = {{Proceedings of the 20th International Colloquium on Theoretical Aspects of Computing (ICTAC'23)}}, year = 2023, editor = {\'Abrah\'am, Erika and Dubslaff, Clemens and Tarifa, Lizeth}, pages = {}, address = {}, organization = {}, publisher = {Springer}, volume = {}, number = {}, series = {LNCS}, month = {}, note = {}, abstract = {We consider \emph{global models} of communicating agents specified as transition systems labelled by \emph{interactions} in which multiple senders and receivers can participate. A \emph{realisation} of such a model is a set of local transition systems---one per agent---which are executed concurrently using synchronous communication. Our core challenge is how to check whether a global model is realisable and, if it is, how to synthesise a realisation. We identify and compare two variants to realise global interaction models, both relying on bisimulation equivalence. Then we investigate, for both variants, \emph{realisability conditions} to be checked on global models. We propose a synthesis method for the construction of realisations by grouping locally indistinguishable states. The paper is accompanied by a tool that implements realisability checks and synthesises realisations.} } @INPROCEEDINGS{PBDTJ23, author = {P\"a{\ss}ler, Juliane and ter Beek, Maurice H. and Damiani, Ferruccio and Tapia Tarifa, S. Lizeth and Johnsen, Einar Broch}, title = {{Formal Modelling and Analysis of a Self-Adaptive Robotic System}}, booktitle = {{Proceedings of the 18th International Conference on Integrated Formal Methods (iFM'23)}}, year = 2023, editor = {Herber, Paula and Wijs, Anton}, pages = {}, address = {}, organization = {}, publisher = {Springer}, volume = {}, number = {}, series = {LNCS}, month = {}, abstract = {Self-adaptation is a crucial feature of autonomous systems that must cope with uncertainties in, e.g., their environment and their internal state. Self-adaptive systems are often modelled as two-layered systems with a \emph{managed} subsystem handling the domain concerns and a \emph{managing} subsystem implementing the adaptation logic. We consider a case study of a self-adaptive robotic system; more concretely, an autonomous underwater vehicle (AUV) used for pipeline inspection. In this paper, we model and analyse it with the feature-aware probabilistic model checker ProFeat. The functionalities of the AUV are modelled in a feature model, capturing the AUV's variability. This allows us to model the managed subsystem of the AUV as a family of systems, where each family member corresponds to a valid feature configuration of the AUV. The managing subsystem of the AUV is modelled as a control layer capable of dynamically switching between such valid feature configurations, depending both on environmental and internal conditions. We use this model to analyse probabilistic reward and safety properties for the AUV.}, note = {} } @article{DBLP:journals/lmcs/BezhanishviliCG22, author = {Nick Bezhanishvili and Vincenzo Ciancia and David Gabelaia and Gianluca Grilletti and Diego Latella and Mieke Massink}, title = {Geometric Model Checking of Continuous Space}, journal = {Log. Methods Comput. Sci.}, volume = {18}, number = {4}, year = {2022}, url = {https://doi.org/10.46298/lmcs-18(4:7)2022}, doi = {10.46298/lmcs-18(4:7)2022} } @inproceedings{DBLP:conf/fm/CianciaGLMV23, author = {Vincenzo Ciancia and Jan Friso Groote and Diego Latella and Mieke Massink and Erik P. de Vink}, editor = {Marsha Chechik and Joost{-}Pieter Katoen and Martin Leucker}, title = {Minimisation of Spatial Models Using Branching Bisimilarity}, booktitle = {Proceedings of Formal Methods (FM'23)}, series = {Lecture Notes in Computer Science}, volume = {14000}, pages = {263--281}, publisher = {Springer}, year = {2023}, url = {https://doi.org/10.1007/978-3-031-27481-7\_16}, doi = {10.1007/978-3-031-27481-7\_16} } @INPROCEEDINGS{Ciancia23, author = {Ciancia, Vincenzo and Gabelaia, David and Latella, Diego and Messink, Mieke and de Vink, Erik P.}, title = {{On Bisimilarity for Polyhedral Models and SLCS}}, booktitle = {{Proceedings of FORTE'23}}, year = 2023, editor = {Marieke Huisman and Ant\'onio Ravara}, pages = {132--151}, address = {}, organization = {}, publisher = {Springer}, volume = {}, number = {}, series = {}, month = mar, note = {} } @InProceedings{eumas2023, author = {Bergenti, Federico AND Monica, Stefania AND Petrosino, Giuseppe}, title = {A Comprehensive Presentation of the {Jadescript} Agent-Oriented Programming Language}, booktitle = {EUMAS 2023: Multi-Agent Systems}, series = {Lecture Notes in Computer Science}, volume = {14282}, pages = {100--115}, publisher = {Springer}, year = {2023}, doi = {10.1007/978-3-031-43264-4_7}, abstract = {Jadescript is an agent-oriented programming language based on JADE that aims to become a dependable tool for the construction of industrial-strength multi-agent systems. This paper contributes to this objective by providing researchers and practitioners with a comprehensive description of Jadescript that discusses the most relevant features attained in several years of continuous development. In particular, this paper focuses on how Jadescript promotes the adoption of some ideas taken from agent-oriented programming by providing direct support for agent-oriented abstractions, like messages and ontologies, by encouraging the use of event-driven programming to govern interactions, and by allowing fine-grained task management using behaviours. Finally, to illustrate the practical applicability of Jadescript, this paper presents in detail the implementation of a well-known election algorithm traditionally used to coordinate distributed systems.} } @InProceedings{icaart2023, author = {Petrosino, Giuseppe AND Monica, Stefania AND Bergenti, Federico}, title = {Cross-Paradigm Interoperability Between {Jadescript} and {Java}}, booktitle = {Proceedings of the 15th International Conference on Agents and Artificial Intelligence - Volume 1: ICAART}, pages = {165--172}, publisher = {SciTePress}, year = {2023}, doi = {10.5220/0011619300003393}, abstract = {Jadescript is a recent language for practical agent-oriented programming that aims at easing the development of multi-agent systems for real-world applications. Normally, these applications require extensive and structured reuse of existing software modules, which are commonly developed using object-oriented or legacy technologies. Jadescript has been originally designed to ease the translation to Java and, as such, it natively eases the interoperability with Java, and therefore, with mainstream and legacy technologies. This paper overviews the features that have been recently added to Jadescript to support effective two-way interoperability with Java. Moreover, this paper thoroughly discusses the main ideas behind such features by framing them in a comparison with related work, and by outlining possible directions for further developments.} } @Article{postwoa2022, author = {Petrosino, Giuseppe AND Monica, Stefania AND Bergenti, Federico}, title = {Effective handling of exceptional situations in robust software agents}, journal = {Intelligenza Artificiale}, volume = {17}, number = {1}, pages = {37--49}, year = {2023}, publisher = {IOS Press}, doi = {10.3233/IA-230003}, abstract = {Software agents are normally expected to operate in open and dynamic environments, and therefore they are often supposed to face situations that significantly deviate from the nominal course of events. The effective management of exceptional situations is of paramount importance to provide agents with the needed means to operate in their environments, mostly because these situations should be considered as the norm in open and dynamic environments. This paper presents some recent additions to the Jadescript agent-oriented programming language that were specifically designed to provide agents with the needed capabilities to effectively detect and manage exceptional situations. The first part of this paper motivates the need of sophisticated exception handling capabilities, also by relating the proposed language features with the state of the art documented in the literature. Then, the second part of this paper discusses the proposed language features, also considering the conceptual similarities and differences with the related features normally available in mainstream programming languages. In particular, the proposed language features are presented in terms of three language improvements: the general-purpose support to handle exceptions, the specific support to handle behaviour failures, and the specific support to handle stale messages. Finally, before concluding with some indications on future research activities, the third part of this paper describes a concrete example intended to practically present the actual use of the new language features.} } @InProceedings{woa2022, author = {Petrosino, Giuseppe AND Monica, Stefania AND Bergenti, Federico}, title = {Robust Software Agents with the {Jadescript} Programming Language}, booktitle = {WOA 2022: 23rd Workshop ``From Objects to Agents''}, series = {CEUR Workshop Proceedings}, volume = {3261}, pages = {194--208}, publisher = {RWTH Aachen}, year = {2022}, url = {https://ceur-ws.org/Vol-3261/paper15.pdf}, abstract = {This paper discusses several recent additions to the Jadescript agent-oriented programming language that regard the effective detection and handling of exceptional and erroneous situations at runtime. These new features were introduced to better support the mission-critical level of robustness that software agents are normally demanded to exhibit. The description of these new features is supported by an analysis of the state of the art of exception handling in programming languages, and it is complemented by a discussion on planned future developments. First, the novel exception handling mechanism introduced in Jadescript is presented, and the conceptual similarities and differences with the exception handling mechanisms normally provided by mainstream programming languages are emphasized. Second, the recent additions to Jadescript designed to support failures in behaviours are described, and these additions are related to the novel exception handling mechanism. Finally, the recent language support to manage stale messages using dedicated message handlers is presented and discussed.} } @InProceedings{dcai2022, author = {Petrosino, Giuseppe AND Monica, Stefania AND Bergenti, Federico}, title = {Delayed and Periodic Execution of Tasks in Jadescript Programming Language}, booktitle = {DCAI 2022: Distributed Computing and Artificial Intelligence, 19th International Conference}, series = {Lecture Notes in Networks and Systems}, volume = {583}, pages = {50--59}, publisher = {Springer}, year = {2022}, doi = {978-3-031-20859-1_6}, abstract = {Software agents are expected to timely act and to dynamically plan their activities, for example, to solve the complex collaboration problems of many real-world applications. The collaboration among agents requires the ability to reason about time to dynamically coordinate and to effectively adjust the frequency of periodic actions and reactions. For these and related reasons, an agent-oriented programming language is demanded to provide the programmer with effective means to schedule the execution of delayed and periodic tasks. This paper describes the new datatypes, and the related changes to some language constructs, that have been recently added to the Jadescript programming language to allow agents to effectively manage the dynamic scheduling of delayed and periodic tasks.} }