This special section of the International Journal on Software and Systems Modeling (SoSyM) contains a selection of the best papers accepted at the 17th edition of the international conference series on Formal Aspects of Component Software (FACS). This conference was held online on October 28–29, 2021.

The aim of the conference series is to study how formal methods can be applied to component-based software and system development. Component-based software development proposes sound engineering principles and techniques to cope with the complexity of modern software systems. Many challenging conceptual and technological issues remain in component-based software development theory and practice. Furthermore, the advent of service-oriented and cloud computing, cyber-physical systems, and the Internet of Things comes with new challenges, such as quality of service and robustness to withstand faults, which require revisiting established concepts and developing new ones. Formal methods have provided foundations for component-based software through research on mathematical models for components, composition and adaptation, and rigorous approaches to verification, deployment, testing, and certification.

After the FACS’21 conference took place, the five best papers were selected, and the authors of these papers were invited to submit a revised and extended version of their work to this special section. After a meticulous review process, we finally accepted three of the five invited papers. Here is a short description of these papers:

  • Composable partial multiparty session types for open systems by Claude Stolze, Marino Miculan, and Pietro Di Gianantonio. This paper introduces partial sessions and partial (multiparty) session types, extending global session types with the possibility to type also open systems, i.e., sessions with missing participants. Sessions with the same name but observed by different participants can be merged if their types are compatible. In this case, the type for the unified session can be derived compositionally from the types of components. To this end, the authors provide a merging algorithm, which allows the detection of incompatible types, due to miscommunications or deadlocks, as early as possible. This differs from usual session type systems which delay all the checks to when the system is completed. Therefore, in this theory the distinction between local and global types vanishes: local types correspond to partial session types for sessions with a single participant, and global types correspond to finalized partial session types, i.e., in which no participant is missing. This paper also generalises the notion of progress to accommodate the case when a partial session cannot progress not due to a deadlock, but to some missing participant.

  • Span(Graph): a canonical feedback algebra of open transition systems by Elena Di Lavore, Alessandro Gianola, Mario Román, Nicoletta Sabadini, and Pawel Sobocinski. This paper focuses on Span(Graph), an algebra for open transition systems originally introduced by Katis, Sabadini and Walters. This paper first shows that this algebra satisfies a universal property, which is a justification of the canonicity of this model of concurrency. The universal property is also of interest, because it is a formal demonstration of the relationship between feedback and state. Indeed, feedback categories, also proposed by Katis, Sabadini and Walters, are a weakening of traced monoidal categories, with various applications in computer science. A state bootstrapping technique, which has appeared in several different contexts, yields free such categories. This paper shows that Span(Graph) arises in this way, being the free feedback category over Span(Set). Given that the latter can be seen as an algebra of predicates, the algebra of open transition systems thus arises as the result of bootstrapping state to that algebra. Finally, this paper generalizes feedback categories endowing state spaces with extra structure: this extends the framework from mere transition systems to automata with initial and final states.

  • Linear parallel algorithms to compute strong and branching bisimilarity by Jan Martens, Jan Friso Groote, Lars van den Haak, Pieter Hijma, and Anton Wijs. The notion of bisimilarity for Kripke structures and Labelled Transition Systems (LTSs) is commonly used to define behavioural equivalence. Deciding this equivalence is essential for modelling and verifying discrete event systems. Kanellakis and Smolka proposed a partition refinement algorithm for obtaining the bisimilarity relation for Kripke structures. The proposed algorithm has a run time complexity of O(nm) where n is the number of states and m is the number of transitions of the input. Later, a more sophisticated refinement algorithm running in O(mlogn) steps was proposed by Paige and Tarjan. This paper presents the first parallel algorithms that decide strong and branching bisimilarity in linear time. More precisely, if a transition system has n states, m transitions, and |Act| action labels, an algorithm is introduced that decides strong bisimilarity in \(O(n + |Act|)\) time on max(n, m) processors, and an algorithm that decides branching bisimilarity in \(O(n + |Act|)\) time using up to \(max(n^2,m,|Act|n)\) processors.

Many people have contributed to the success of this special section. Beyond the authors of the papers, we would like to thank both the members of the Program Committee of the FACS’21 conference and the additional reviewers who kindly agreed to help us with the reviewing of the papers in this special section. All carried out an excellent job during this demanding process. We are also grateful to Martin Schindler for his guidance during the elaboration of this special section. We hope that these papers will bring the reader novel insights and ideas.

The SoSyM Guest Editor