The world we inhabit is increasingly shaped—and structured—by digital technologies that act autonomously, both on our behalf and to fulfill our needs. This transformation raises profound ethical concerns about the potential impact of interactions between humans and autonomous systems on the values underpinning our societies.

Modern digital systems pose risks to humans, society, and the environment. There is a flourishing of guidelines, recommendations, laws, and regulations, but also of standards that try to regulate and alleviate the lack of good practices for the governance, management, and quality of AI systems. However, having just a mark certifying that the system passed some checks is not enough and is fragile to the ethics washing problem. The objective of this work is to go beyond compliance to standards toward an ethics label that enables users to understand the impact of systems on human, societal, and environmental values, both during system development and usage. To build the ethics label, we analyze guidelines, recommendations, laws and regulations, and quality standards. We validate the proposed ethics label through (i) a proof-of-concept application to the social assistive robotics domain, and (ii) interviews with experts from both academia and industry. We contribute an ethics label for modern digital systems that promote transparency and user awareness, and enable users to select systems that meet their subjective ethical preferences. We discuss the problem of ethics washing and propose an ethics label as a means to foster transparency and raise user awareness.

Background. Autonomous systems, whether AI-enabled or not, are ubiquitous and pervasive in our daily lives. While their adoption and use bring many benefits, they also pose significant ethical challenges. Objective. The objective of this work is to contribute a reference architecture for ethical-aware autonomous systems, focusing on their interaction and collaboration with humans, being them proactive, reactive or passive in the interaction with the systems. Method. To define the architecture, we analyzed scientific papers in the field, guidelines and recommendations, as well as laws and regulations. We then applied this acquired knowledge to build the reference architecture. The results of this work were validated through expert interviews and a scenario-based evaluation. Results. We contribute (i) a definition of ethical-aware autonomous systems, (ii) requirements for ethical-aware autonomous systems, and (iii) a reference architecture for ethical-aware autonomous systems. Our reference architecture is intended to help system and software engineers to design autonomous or intelligent systems that should interact and operate with humans in ethically sensitive contexts such as healthcare, social robotics, and assistive technologies. Conclusion. We believe that this work will assist software architects and engineers in designing and developing autonomous systems that should interact and collaborate with humans while respecting values important to individuals, society, and the environment.

The presence of autonomous systems is growing at a fast pace and it is impacting many aspects of our lives. Designed to learn and act independently, these systems operate and perform decision-making without human intervention. However, they lack the ability to incorporate users’ ethical preferences, which are unique for each individual in society and are required to personalize the decision-making processes. This reduces user trust and prevents autonomous systems from behaving according to the moral beliefs of their end-users. When multiple systems interact with differing ethical preferences, they must negotiate to reach an agreement that satisfies the ethical beliefs of all the parties involved and adjust their behavior consequently. To address this challenge, this paper proposes RobEthiChor , an approach that enables autonomous systems to incorporate user ethical preferences and contextual factors into their decision-making through ethics-based negotiation. RobEthiChor features a domain-agnostic reference architecture for designing autonomous systems capable of ethic-based negotiating. The paper also presents RobEthiChor-Ros , an implementation of RobEthiChor within the Robot Operating System (ROS), which can be deployed on robots to provide them with ethics-based negotiation capabilities. To evaluate our approach, we deployed RobEthiChor-Ros on real robots and ran scenarios where a pair of robots negotiate upon resource contention. Experimental results demonstrate the feasibility and effectiveness of the system in realizing ethics-based negotiation. RobEthiChor allowed robots to reach an agreement in more than 73 % of the scenarios with an acceptable negotiation time (0.67s on average). Experiments also demonstrate that the negotiation approach implemented in RobEthiChor is scalable.

Large Language Models (LLMs) are increasingly integrated into software engineering (SE) tools for tasks that extend beyond code synthesis, including judgment under uncertainty and reasoning in ethically significant contexts. We present a fully automated framework for assessing ethical reasoning capabilities across 16 LLMs in a zero-shot setting, using 30 real-world ethically charged scenarios. Each model is prompted to identify the most applicable ethical theory to an action, assess its moral acceptability, and explain the reasoning behind their choice. Responses are compared against expert ethicists’ choices using inter-model agreement metrics. Our results show that LLMs achieve an average Theory Consistency Rate (TCR) of 73.3% and Binary Agreement Rate (BAR) on moral acceptability of 86.7%, with interpretable divergences concentrated in ethically ambiguous cases. A qualitative analysis of free-text explanations reveals strong conceptual convergence across models despite surface-level lexical diversity. These findings support the potential viability of LLMs as ethical inference engines within SE pipelines, enabling scalable, auditable, and adaptive integration of user-aligned ethical reasoning. Our focus is the Ethical Interpreter component of a broader profiling pipeline: we evaluate whether current LLMs exhibit sufficient interpretive stability and theory-consistent reasoning to support automated profiling.

As testified by new regulations like the European AI Act, worries about the human and societal impact of (autonomous) software technologies are becoming of public concern. Human, societal, and environmental values, alongside traditional software quality, are increasingly recognized as essential for sustainability and long-term well-being. Traditionally, systems are engineered taking into account business goals and technology drivers. Considering the growing awareness in the community, in this article, we argue that engineering of systems should also consider human, societal, and environmental drivers. Then, we identify the macro and technological challenges by focusing on humans and their role while co-existing with digital systems. The first challenge considers humans in a proactive role when interacting with digital systems, i.e., taking initiative in making things happen instead of reacting to events. The second concerns humans having a reactive role in interacting with digital systems, i.e., humans interacting with digital systems as a reaction to events. The third challenge focuses on humans with a passive role, i.e., they experience, enjoy or even suffer the decisions and/or actions of digital systems. The fourth challenge concerns the duality of trust and trustworthiness, with humans playing any role. Building on the new human, societal, and environmental drivers and the macro and technological challenges, we identify a research roadmap of digital systems for humanity. The research roadmap is concretized in a number of research directions organized into four groups: development process, requirements engineering, software architecture and design, and verification and validation.

The rise of AI-based and autonomous systems is raising concerns and apprehension due to potential negative repercussions arising from their behavior or decisions. These systems must be designed to comply with the human contexts in which they will operate. To this extent, Townsend et al. (2022) introduce the concept of SLEEC (social, legal, ethical, empathetic, or cultural) rules that aim to facilitate the formulation, verification, and enforcement of the rules AI-based and autonomous systems should obey. They lay out a methodology to elicit them and to let philosophers, lawyers, domain experts, and others to formulate them in natural language. To enable their effective use in AI systems, it is necessary to translate these rules systematically into a formal language that supports automated reasoning. In this study, we first conduct a linguistic analysis of the SLEEC rules pattern, which justifies the translation of SLEEC rules into classical logic. Then we investigate the computational complexity of reasoning about SLEEC rules and show how logical programming frameworks can be employed to implement SLEEC rules in practical scenarios. the result is a readily applicable strategy for implementing AI systems that conform to norms expressed as SLEEC rules.

This paper briefly outlines a high-level architecture of a context-aware ethics-based negotiation approach in which autonomous systems utilize user ethical profiles, together with contextual factors and user status, to control their autonomy while collaboratively negotiating to reach an ethical agreement that satisfies the ethical beliefs of all parties involved.

Abstract Protecting privacy and ethics of citizens is among the core concerns raised by an increasingly digital society. Profiling users is common practice for software applications triggering the need for users, also enforced by laws, to manage privacy settings properly. Users need to properly manage these settings to protect personally identifiable information and express personal ethical preferences. This has shown to be very difficult for several concurrent reasons. However, profiling technologies can also empower users in their interaction with the digital world by reflecting personal ethical preferences and allowing for automatizing/assisting users in privacy settings. In this way, if properly reflecting users’ preferences, privacy profiling can become a key enabler for a trustworthy digital society. We focus on characterizing/collecting users’ privacy preferences and contribute a step in this direction through an empirical study on an existing dataset collected from the fitness domain. We aim to understand which set of questions is more appropriate to differentiate users according to their privacy preferences. The results reveal that a compact set of semantic-driven questions (about domain-independent privacy preferences) helps distinguish users better than a complex domain-dependent one. Based on the outcome, we implement a recommender system to provide users with suitable recommendations related to privacy choices. We then show that the proposed recommender system provides relevant settings to users, obtaining high accuracy.

Abstract GitHub provides developers with a practical way to distribute source code and collaboratively work on common projects. To enhance account security and privacy, GitHub allows its users to manage access permissions, review audit logs, and enable two-factor authentication. However, despite the endless effort, the platform still faces various issues related to the privacy of its users. This paper presents an empirical study delving into the GitHub ecosystem. Our focus is on investigating the utilization of privacy settings on the platform and identifying various types of sensitive information disclosed by users. Leveraging a dataset comprising 6,132 developers, we report and analyze their activities by means of comments on pull requests. Our findings indicate an active engagement by users with the available privacy settings on GitHub. Notably, we observe the disclosure of different forms of private information within pull request comments. This observation has prompted our exploration into sensitivity detection using a large language model and BERT, to pave the way for a personalized privacy assistant. Our work provides insights into the utilization of existing privacy protection tools, such as privacy settings, along with their inherent limitations. Essentially, we aim to advance research in this field by providing both the motivation for creating such privacy protection tools and a proposed methodology for personalizing them.

The Android OS market is experiencing a growing share globally. It is becoming the mobile platform of choice for an increasing number of users. People rely on Android mobile devices for surfing the web, purchasing products, or to be part of a social network. The large amount of personal information that is exchanged makes privacy an important concern. As a result, the trustability of mobile apps is a fundamental aspect to be considered, particularly with regard to meeting the expectations of end users. The rigidities of the Android permission model confine end users into a secondary role, offering the only option of choosing between either privacy or functionalities. In this paper, we aim at improving the trustability of Android apps by proposing a user-centric approach to the flexible management of Android permissions. The proposed approach empowers end users to selectively grant permission by specifying (i) the desired level of permissions granularity and (ii) the specific features of the app in which the chosen permission levels are granted. Four experiments have been designed, conducted, and reported for evaluating it. The experiments consider performance, usability, and acceptance from both the end user's and developer's perspective. Results confirm confidence on the approach.

In the near future we will be surrounded by a virtually infinite number of software applications that provide services in the digital space. This situation radically changes the way software will be produced and used: (i) software is increasingly produced according to specific goals and by integrating existing software; (ii) the focus of software production will be shifted towards reuse of third-parties software, typically black-box, that is often provided without a machine readable documentation. The evidence underlying this scenario is that the price to pay for this software availability is a lack of knowledge on the software itself, notably on its interaction behaviour A producer will operate with software artifacts that are not completely known in terms of their functional and non-functional characteristics. The general problem is therefore directed to the ability of devising (architectural/component) models that will let the artifacts interact to reach the goal. This talk focuses on models, techniques and tools for integration code and component interaction protocols which allow to deal with partial knowledge and automatically produce correctby- construction service-oriented systems with respect to functional and non functional goals.

No abstract available.

The Future Internet is becoming a reality, providing a large-scale computing environments where a virtually infinite number of available services can be discovered and composed so to fit users' needs. In order to enable this large-scale and evolvable computing environment, the ability to automatically compose and dynamically coordinate heterogeneous software services is of paramount importance. Service choreographies are an emergent Service Engineering (SE) approach to compose together and coordinate services in a distributed way. They represent a global specification of the interactions between the participant services. Choreographies will play a central role in Future Internet as an effective means to allow heterogeneous services to suitably collaborate. This new ideas paper briefly describes the experience of choreography development that we have been doing so far within the CHOReOS project, and proposes the novel idea we are currently investigating within the IDEAS project to achieve choreography adaptation and evolution through complex data mappings.

Ubiquitous and pervasive computing promotes the creation of an environment where Networked Systems (NSs) eternally provide connectivity and services without requiring explicit awareness of the underlying communications and computing technologies. In this context, achieving interoperability among heterogeneous NSs represents an important issue. In order to mediate the NSs interaction protocol and solve possible mismatches, connectors are often built. However, connector development is a never-ending and error-prone task and prevents the eternality of NSs. For this reason, in the literature, many approaches propose the automatic synthesis of connectors. However, solving the connector synthesis problem in general is hard and, when possible, it results in a monolithic connector hence preventing its evolution. In this paper, we define a method for the automatic synthesis of modular connectors, each of them expressed as the composition of independent mediators. A modular connector, as synthesized by our method, supports connector evolution and performs correct mediation.

This panel will discuss what characterizes the publication process in the software engineering community and debate how it serves the needs of the community, whether it is fair - e.g. valuable work gets published and mediocre work rejected - and highlight the obstacles for young scientists. The panel will conclude with a discussion on suggested next steps.

Software is increasingly produced according to a certain goal and by integrating existing software produced by third-parties, typically black-box, and often provided without a machine readable documentation. This implies that development processes of the next future have to explicitly deal with an inherent incompleteness of information about existing software, notably on its behaviour. Therefore, on one side a software producer will less and less know the precise behaviour of a third party software service, on the other side she will need to use it to build her own application. In this paper we present an innovative development process to automatically produce dependable software systems by integrating existing services under uncertainty and according to the specied goal. Moreover, we (i) discuss important challenges that must be faced while producing the kind of systems we are targeting, (ii) give an overview of the state of art related to the identied challenges, and finally (iii) provide research directions to address these challenges.

The papers in this special section contain extended versions of selected papers from the 31st ACM/IEEE International Conference on Software Engineering (ICSE), held 20-22 May 2009 in Vancouver, British Columbia, Canada.

In the next future we will be surrounded by a virtually infinite number of software applications that provide computational software resources in the open Globe. This will radically change the way software will be produced and used. Users will be keen on producing their own piece of software, by also reusing existing software, to better satisfy their needs, therefore with a goal oriented, opportunistic use in mind. The produced software will need to be able to evolve, react and adapt to a continuously changing environment, while guaranteeing dependability. The strongest adversary to this view is the lack of knowledge on the software's structure, behavior, and execution context. Despite the possibility to extract observational models from existing software, a producer will always operate with software artifacts that exhibit a degree of uncertainty in terms of their functional and non functional characteristics. We believe that uncertainty can only be controlled by making it explicit and by using it to drive the production process itself. In this paper, we introduce a novel paradigm of software production process that explores available software and assesses its degree of uncertainty in relation to the opportunistic goal G, assists the producer in creating the appropriate integration means towards G, and validates the quality of the integrated system with respect to G and the current context.

Currently, software testing is mainly carried on independently from software architecture-related information. Some approaches propose to perform integration and regression testing with respect to software architecture descriptions, but less attention has been paid to analysing software architecture in order to develop a less costly and time-consuming test plan that covers the requirements of the system of interest. If on one side, it is well known that providing an effective test plan is crucial to software quality, on the other side software testing is extremely difficult because it stems from the complexity of current software systems.

The CONNECT European project that started in February 2009 aims at dropping the interoperability barrier faced by todaypsilas distributed systems. It does so by adopting a revolutionary approach to the seamless networking of digital systems, that is, synthesizing on the fly the connectors via which networked systems communicate. CONNECT then investigates formal foundations for connectors together with associated automated support for learning, reasoning about and adapting the interaction behavior of networked systems.

Web-services are broadly considered as an effective means to achieve interoperability between heterogeneous parties of a business process and offer an open platform for developing new composite web-services out of existing ones. In the literature many approaches have been proposed with the aim to automatically compose web-services. All of them assume that, along with the web-service signature, some information is provided about how clients interacting with the web-service should behave when invoking it.

Introduced in the early stages of software development, the Charmy framework assists the software architect in making and evaluating architectural choices. Rarely, the software architecture of a system can be established once and forever. Most likely poorly defined and understood architectural constraints and requirements force the software architect to accept ambiguities and move forward to the construction of a suboptimal software architecture. Charmy aims to provide an easy and practical tool for supporting the iterative modeling and evaluation of software architectures. From an UML-based architectural design, an executable prototype is automatically created. Charmy simulation and model checking features help in understanding the functioning of the system and discovering potential inconsistencies of the design. When a satisfactory and stable software architecture is reached, Java code conforming to structural software architecture constraints is automatically generated through suitable transformations. The overall approach is tool supported.

In this paper we present a static analysis approach for inspecting Java programs and characterizing them with respect to their resource consumption in a given execution environment. We target, in particular, resource constrained devices that are characterized by resource scarcity and limited computational power. The focus of this paper is on a parametrical abstract resource analyzer that performs the actual analysis and is supported by a resource model that allows us to abstract application behavior in terms of its resource needs. The presented components are integrated in a larger framework that provides a complete system for reasoning and adapting Java programs with respect to heterogeneous contexts.

SYNTHESIS is a tool for automatically assembling correct and distributed component-based systems. In our context, a system is correct when it is deadlock-free and performs only specified component interactions. In order to automatically synthesize the correct composition code, SYNTHESIS takes as input an high-level behavioural description for each component that must form the system to be built and a specification of the component interactions that must be enforced in the system. The automatically derived composition code is implemented as a set of distributed component wrappers that cooperatively interact with each other and with their wrapped components in order to prevent possible deadlocks and make the composed system exhibit only the specified interactions. The current version of SYNTHESIS supports two possible development platforms: Microsoft COM/DCOM, and EJB (Enterprise Java Beans).

This paper presents the tool DESERT that allows the generation of decentralized monitoring systems for component based applications.

Software models are, in most cases, considered as functional abstractions of systems. They represent the backbone of transformational processes aimed at code generation. On the other end, modeling is a traditional activity in the field of non-functional validation of software/hardware systems, although non-functional models found on different notations (such as Petri Nets) and embed additional information (such as the operational profile) with respect to software models. In this paper we widen the scope of model-driven architecture by introducing a Non-Functional-MDA framework that, beside the typical model transformations for code generation, embeds new types of model transformations that allow to generate non-functional models. For an uniform integration of these practices, we define Platform Independent/Specific Models in the non-functional domain.

We present an approach to provide intrusion detection systems (IDS) facilities into wireless sensors networks (WSN). WSNs are usually composed of a large number of low power sensors. They require a careful consumption of the available energy in order to prolong the lifetime of the network. From the security point of view, the overhead added to standard protocols must be as light as possible according to the required security level. Starting from the DESERT tool (P. Inverardi et al., 2005) which has been proposed for component-based software architectures, we derive a new framework that permits to dynamically enforce a set of properties of the sensors behavior. This is accomplished by an IDS specification that is automatically translated into few lines of code installed in the sensors. This realizes a distributed system that locally detects violation of the sensors interactions policies and is able to minimize the information sent among sensors in order to discover attacks over the network

It is widely recognized that in order to make performance validation an integrated activity along the software lifecycle it is crucial to be supported from automated approaches. Easiness to annotate software models with performance parameters (e.g. the operational profile) and automated translations of the annotated models into "ready-to-validate" models are the key challenges in this direction. Several methodologies have been introduced in the last few years to address these challenges. The tutorial introduces the attendance to the main methodologies for annotating and transforming software models into performance models.

The attendees of ICSE comprise some of the top researchers in software engineering and also many educators of software engineering. Traditionally, however, these two groups do not talk to each other about educational issues. Then there are the practitioners who attend ICSE who have their own opinions about the relevance, strengths, and shortcomings of current software engineering education offered in universities. The goal of this year's track on Software Engineering Education and Training at ICSE is to bring these three communities together to discuss some urgent questions that have profound effect on how we structure our educational programs. Considering the tremendous changes taking place in the software engineering industry, and in the industrial world in general, it seems appropriate to confront the needs of the software engineering educators.Consider just the following increasingly common developments:Outsourcing of software projectsPervasiveness of software in all areas of commerce, industry, and societyIncreasingly distributed platformsOpen-source developmentGlobalization, leading to international (multi-cultural) distributed software teamsHow should these developments change the way we teach software engineering? Should textbooks be updated? Should software engineering play a different role in the computer science curriculum, that is, be more pervasive? How are professors in universities handling these issues?These are some of the questions we address in this track. In particular, we consider current challenges, current solutions, and future challenges. We are pleased to have six distinguished researchers to present their views and fifteen presenters from universities around the world presenting their innovative approaches in their classrooms. We expect lively and active discussion between the speakers and the audience.

Building a distributed system from third-party components introduces a set of problems, mainly related to compatibility and communication. Our approach to solve these problems is to build an adaptor which forces the system to exhibit only a set of safe or desired behaviors. By exploiting an abstract and partial specification of the global behavior that must be enforced, we automatically build a centralized adaptor. It mediates the interaction among components by both performing the specified behavior and, simultaneously, avoiding possible deadlocks. However in a distributed environment it is not always possible or convenient to insert a centralized adaptor. In contrast, building a distributed adaptor might increase the applicability of the approach in a real-scale context. In this paper we show how it is possible to automatically generate a distributed adaptor by exploiting an approach to the definition of distributed IDS (Intrusion Detection Systems) filters developed by us to increase security measures in component based systems. Firstly, by taking into account a high level specification of the global behavior that must be enforced, we synthesize a behavioral model of a centralized adaptor that allows the composed system to only exhibit the specified behavior and, simultaneously, avoid possible unspecified deadlocks. This model represents a lower level specification of the global behavior that is enforced by the adaptor. Secondly, by taking into account the synthesized adaptor model, we generate a set of component filters that validate the centralized adaptor behavior by simply looking at local information. In this way we address the problem of mechanically generating correct and distributed adaptors for real-scale component-based systems.

CHARMY is a framework for designing and validating architectural specifications. In the early stages of the software development process, the CHARMY framework assists the software architect in the design and validation phases. To increase its usability in an industrial context, the tool allows the use of UML-like notations to graphically design the system. Once the design is done, a formal prototype is automatically created for simulation and analysis purposes. The framework provides extensibility mechanisms to enable the introduction of new design and analysis features.

Many formal languages have been proposed so far to describe software architectures (SA), but only very few of them are still supported and used in practical contexts. Many UML profiles and extensions have been provided when UML became a standard, in order to model as much as possible architectural concepts. They allow for an easy integration in industrial processes, however, different analysis techniques and domains still require different notations. In fact, since different communities require different information to be put into a diagram, depending on which architectural design aspects should be represented and analyzed, the idea of an unified UML language for SA is not adequate. Building on these considerations, we propose DUALLY, a core set of UML concepts, well suited for SA modeling, together with a framework which provides extensibility mechanisms to adapt the initial notation, in order to meet different needs.

In this paper we present a compositional reasoning to verify middleware-based software architecture descriptions. We consider a nowadays typical software system development, namely the development of a software application A on a middleware M. Our goal is to efficiently integrate verification techniques, like model checking, in the software life cycle in order to improve the overall software quality. The approach exploits the structure imposed on the system by the software architecture in order to develop an assume-guarantee methodology to reduce properties verification from global to local. We apply the methodology on a non-trivial case study namely the development of a Gnutella system on top of the SIENA event-notification middleware.

Early performance analysis based on queueing network models (QNM) has been often proposed to support software designers during the software development process. These approaches aim at addressing performance issues as early as possible in order to reduce design failures. All of them try to adapt to software systems the well-known system performance analysis methodology. This implies that they assume at design time the availability of information about the hardware platform the software runs on. In recent years, we have proposed a methodology that allows quantitative reasoning on software aspects without considering hardware aspects. In this work, we extend our methodology to encompass a compositional approach to performance analysis of software architecture described by means of UML 2.0 diagrams. The main improvements include the characterization of architectural patterns and of their corresponding QNM pattern; the use of multi-chain queueing network as system target model and the identification of the information needed to parameterize the system model.

Over the last decade, a lot of research has been directed toward integrating performance analysis into the software development process. Traditional software development methods focus on software correctness, introducing performance issues later in the development process. This approach does not take into account the fact that performance problems may require considerable changes in design, for example, at the software architecture level, or even worse at the requirement analysis level. Several approaches were proposed in order to address early software performance analysis. Although some of them have been successfully applied, we are still far from seeing performance analysis integrated into ordinary software development. In this paper, we present a comprehensive review of recent research in the field of model-based performance prediction at software development time in order to assess the maturity of the field and point out promising research directions.

Our research deals with the use of software architecture (SA) as a reference model for testing the conformance of an implemented system with respect to its architectural specification. We exploit the specification of SA dynamics to identify useful schemes of interactions between system components and to select test classes corresponding to relevant architectural behaviors. The SA dynamics is modeled by labeled transition systems (LTSs). The approach consists of deriving suitable LTS abstractions called ALTSs. ALTSs offer specific views of SA dynamics by concentrating on relevant features and abstracting away from uninteresting ones. Intuitively, deriving an adequate set of test classes entails deriving a set of paths that appropriately cover the ALTS. Next, a relation between these abstract SA tests and more concrete, executable tests needs to be established so that the architectural tests derived can be refined into code-level tests. We use the TRMCS case study to illustrate our hands-on experience. We discuss the insights gained and highlight some issues, problems, and solutions of general interest in architecture-based testing.

In recent years the necessity for handling different aspects of the system separately has introduced the need to represent SA (software architectures) from different viewpoints. In particular, behavioral views are recognized to be one of the most attractive features in the SA description, and in practical contexts, state diagrams and scenarios are the most widely used tools to model this view. Although very expressive, this approach has two drawbacks: system specification incompleteness and view consistency. Our work can be put in this context with the aim of managing incompleteness and checking view conformance: we propose the use of state diagrams and scenario models for representing system dynamics at the architectural level; they can be incomplete and we want to prove that they describe, from different viewpoints, the same system behavior. To reach this goal, we use the SPIN model checker and we implement a tool to manage the translation of architectural models in Promela and LTL.

Nowadays component-based technologies offer straightforward ways of building applications from existing components. Although these technologies might differ in terms of the level of heterogeneity among components they support, e.g. CORBA or COM versus J2EE, they all suffer the problem of dynamic integration. That is, once components are successfully integrated in a uniform context how is it possible to check, control and assess that the dynamic behavior of the resulting application will not deadlock? The authors propose an architectural, connector-based approach to this problem. We compose a system in such a way that it is possible to check whether and why the system deadlocks. Depending on the kind of deadlock, we have a strategy that automatically operates on the connector part of the system architecture in order to obtain a suitably equivalent version of the system which is deadlock-free.

Many software projects are based on the integration of independently designed software components that are acquired on the market rather than developed within the project itself. Sometimes interoperability and composition mechanisms provided by component based integration frameworks cannot solve the problem of binary component integration in an automatic way. Notably, in the context of component based concurrent systems, the binary component integration may cause deadlocks within the system. In this paper we present a technique to allow connectors synthesis for deadlock-free component based architectures [2] in a real scale context, namely in the context of COM/DCOM applications. This technique is based on an architectural, connector-based approach which consists of synthesizing a COM/DCOM connector as a COM/DCOM server that can route requests of the clients through a deadlock free policy. This work also provides guide lines to implement an automatic tool that derives the implementation of routing dead-lock-free policy within the connector from the dynamic behavior specification of the COM components. It is then possible to avoid the deadlock by using COM composition mechanisms to insert the synthesized connector within the system while letting the system COM servers unimodified. We present a sucessful application of this technique on the (COM version of the) problem known as "The dining philosophers". Depending on the type of deadlock we have a strategy that automatically operates on the connector part of the system architecture in order to obtain a suitably equivalent version of the system which is deadlock-free.

In this paper we present a verification framework to check properties of full CCS terms. These properties are expressed in an action-based logic, and the proof technique is model checking, based on the transition system corresponding to the CCS term. Our approach also allows some kinds of properties to be proved if the transition systems are infinite. Of course, in these cases we only have a semi-decision method. The idea is to use (a sequence of) finite-state transition systems which approximate the, possibly infinite, transition system corresponding to a term. To this end we define a particular notion of approximation, suitable in proving liveness and safety properties of the process terms. Then we show that the class of provable properties might also depend on the way chains of approximations are built and we provide a set of notions to compare and choose among different approximation chains.

The paper presents an approach to derive test plans for the conformance testing of a system implementation with respect to the formal description of its Software Architecture (SA). The SA describes a system in terms of its components and connections, therefore the derived test plans address the integration testing phase. We base our approach on a Labelled Transition System (LTS) modeling the SA dynamics, and on suitable abstractions of it, the Abstract Labelled Transition Systems (ALTSs). ALTSs oer specic views of the SA dynamics by concentrating on relevant features and abstracting away from uninteresting ones. ALTS is a tool we provide the software architect with allow him/her to focus on relevant behavioral patterns and more easily identify those ones that are more meaningful for validation purposes. Intuitively deriving an adequate set of functional test classes means deriving a set of paths appropriately covering the ALTS. In the paper we describe our approach in the scope of a...

A critical challenge faced by the developer of a software system is to understand whether the system's components correctly integrate. While type theory has provided substantial help in detecting and preventing errors in mismatched static properties, much work remains in the area of dynamics. In particular, components make assumptions about their behavioral interaction with other components, but currently we have only limited ways in which to state those assumptions and to analyze those assumptions for correctness. We have formulated a method that begins to address this problem. The method operates at the architectural level so that behavioral integration errors, such as deadlock, can be revealed early and at a high level. For each component, a specification is given of its interaction behavior. Form this specification, assumptions that the component makes about the corresponding interaction behavior of the external context are automatically derived. We have defined an algorithm that performs compatibility checks between finite representations of a component's context assumptions and the actual interaction behaviors of the components with which it is intended to interact. A configuration of a system is possible if and only if a successful way of matching actual behaviors with assumptions can be found. The state-space complexity of this algorithm is significantly less than that of comparable approaches, and in the worst case, the time complexity is comparable to the worst case of standard rachability analysis.

In this paper we contrast (the core of) four well-known process algebras specifically enriched for the specification and verification of timed systems. The aim of this comparison is twofold. On one hand it permits to gain confidence on how time and time passing are modelled in the four different timed process algebras. On the other hand, it establishes conditions under which mappings from a calculus to another can be provided which preserve (strong bisimulation-based) behavioural equivalence.

Terms finitely representing infinite sequences of finite first-order terms have received attention by several authors. In this paper, we consider the class of recurrent terms proposed by H. Chen and J. Hsiang, and we extend it to allow infinite terms. This extension helps in clarifying the relationships between matching and unification over the class of terms we consider, that we call iterative terms. In fact, it holds that if a term s matches a term t by a substitution Γ, then the limit of iterations of the matching Γ, if it exists, is a most general unifier of s and t. A crucial feature of iterative terms is the notion of maximally-folded normal form that allows for a comprehensive treatment of both finite and infinite iterative terms. In this setting, infinite terms can be simply characterized as limits of sequences of finite terms. For finite terms we positively settle an open problem of H. Chen and J. Hsiang on the number of most general unifiers for a pair of terms.

Software architectures can play a role in improving the testing process of complex systems. In particular descriptions of the software architecture can be useful to drive integration testing, since they supply information about how the software is structured in parts and how those parts (are expected to) interact. We propose to use formal architectural descriptions to model the "interesting" behaviour of the system. This model is at a right level of abstraction to be used as a formal base on which integration test strategies can be devised. Starting from a formal description of the software architecture (given in the CHAM formalism), we first derive a graph of all the possible behaviours of the system in terms of the interactions between its components. This graph contains altogether the information we need for the planning of integration testing. On this comprehensive model, we then identify a suitable set of reduced graphs, each highlighting specific architectural properties of the system. These reduced graphs can be used for the generation of integration tests according to a coverage strategy, analogously to what happens with the control and data flow graphs in unit testing.

We are exploring an approach to formally specifying and analyzing software architectures that is based on viewing software systems as chemicals whose reactions are controlled by explicitly stated rules. This powerful metaphor was devised in the domain of theoretical computer science by Bana/spl circ/tre and Le Me/spl acute/tayer (1990) and then reformulated as the CHAM (CHemical Abstract Machine) by Berry and Boudol (1992). The CHAM formalism provides a framework for developing operational specifications that does not bias the described system toward any particular computational model. It also encourages the construction and use of modular specifications at different levels of detail. We illustrate the use of the CHAM for architectural description and analysis by applying it to two different architectures for a simple but familiar software system, the multiphase compiler.>

Abstract There can be different views of a concurrent distributed system, depending on who observes it. The final user may just want to know how the system behaves in terms of its possible sequences of actions, while the designer may want to know what are the sequential components of a system or how are they distributed in space. In other words, there is not a widely accepted single semantic model for concurrent systems. This paper describes a parametric verification tool for process description languages. It performs a symbolic execution of processes at different levels of abstraction and verifies deadlock and reachability properties. The tool also provides facilities to check behavioural equivalences. In addition to the classical interleaving semantics, truly concurrent approaches based on the notion of causality and locality are considered. This allows us to compare the expressive power of different models within the same environment. In this respect, we have verified many of the examples given in the literature using our tool.

Abstract We present a translation of Ada configuration constructs, in a higher order, impredicatively typed, functional language (HOTFUL) with subtypes. The aim of this work is to provide an expressive executable semantics for Ada configuration constructs, and to verify the suitability of the chosen HOTFUL for such a task. In particular, we address the practicability of the approach when dealing with the development of a whole complex system, as well as the description of single modular units. After giving the detailed rules for the translation, we compare our approach with what could be obtained selecting a different typed language as “target”, namely the predicative type system of Standard ML.

Abstract An approach to achieving dynamic reconfiguration within the framework of Ada1 is described. A technique for introducing a kernel facility for dynamic reconfiguration in Ada is illustrated, and its implementation using the Verdix VADS 5.5 Ada compiling system on a Sun3–120 running the 4.3 BSD Unix operating system is discussed. This experimental kernel allows an Ada program to change its own configuration dynamically, linking new pieces of code at run‐time. It is shown how this dynamic facility can be integrated consistently at the Ada language level, without introducing severe inconsistencies with respect to the Standard semantics.

The paper presents a system to support prototyping in a deductive database management context. First, the basic entities and activities involved in the prototyping process are recast into a knowledge base framework. Then, the system GEDBLOG is introduced, illustrating how its features can be used to provide a suitable support to the defined environment. The design and prototyping of a graphic application demonstrates the approach.>