Generating a class integration test order (CITO) is essential to reduce the overhead of test stub construction (the primary cost in integration testing) and to ensure system reliability in complex software systems. Although reinforcement learning (RL) has shown promise in automating CITO generation, existing methods suffer from unstable policy learning and limited robustness against structural perturbations and defect injection. These challenges stem from insufficient reward shaping and the lack of reliable oracles for validation. To address these limitations, we propose LM-CITO, a stability-aware RL framework that integrates Lyapunov-guided reward shaping with semantic validation through metamorphic testing (MT). Specifically, we design a Lyapunov energy function over class dependency graphs to promote monotonic structural convergence during training, and define metamorphic relations (MRs) to verify behavioral consistency under controlled perturbations. Extensive experiments on six real-world systems demonstrate that LM-CITO consistently produces more effective policies, yielding CITOs with significantly reduced stubbing costs compared to baseline models. Furthermore, MT verifies the capability of our MRs to detect defects in 19 injected bug variants, confirming the robustness of LM-CITO under various fault-induced perturbations. These results highlight the synergy of stability guidance and MR-based validation, offering an effective, principled solution for oracle-free RL in software testing.

Class Integration Test Order (CITO) generation is essential to minimize testing cost in object-oriented software.Traditional methods based on static dependencies often producesuboptimal results, while recent approaches that incorporatedynamic dependencies typically neglect accurate stubbing costestimation and face scalability challenges. We propose DyCITO+,an extension of DyCITO, which originally modeled CITO generationas a Reinforcement Learning (RL) problem using Qlearning.However, DyCITO relies on tabular methods, and thislimits its scalability. DyCITO+ addresses this by introducingthree Deep Reinforcement Learning (DRL) algorithms: DeepQ-Network (DQN), Proximal Policy Optimization (PPO), andAdvantage Actor-Critic (A2C), to handle the complexity oflarge-scale systems more effectively. DyCITO+ builds on thedynamic dependency analysis mechanism from DyCITO, whichcaptures more accurate runtime relationships, including interfaceimplementation, abstract class inheritance, method overriding,and multilevel inheritance. We evaluated DyCITO+ on eightJava programs of varying sizes. The results show that DyCITO+significantly improves the scalability and effectiveness of CITOgeneration. Among the three DRL methods, A2C consistentlyproduces the lowest overall stubbing complexity, particularly inmedium- and large-scale systems.

Requirements elicitation is still one of the most challenging activities of the requirements engineering process due to the difficulty requirements analysts face in understanding and translating complex needs into concrete requirements that directly impact the quality of the software to be developed.Although automated tools allow for assessing the syntactic quality of requirements, evaluating semantic metrics (e.g., language clarity, internal consistency) remains a manual and time-consuming activity.This paper explores how LLMs can help automate requirements elicitation within agile frameworks, where requirements are defined as user stories.We used 10 state-of-theart LLMs to investigate their ability to generate user stories automatically by emulating customer interviews.We evaluated the quality of user stories generated by LLMs, comparing it with the quality of user stories generated by humans (domain experts and students).We also explored whether and how LLMs can be used to automatically evaluate the semantic quality of user stories.Our results indicate that LLMs can generate user stories similar to humans in terms of coverage and stylistic quality, but exhibit lower diversity and creativity.Although LLMgenerated user stories are generally comparable in quality to those created by humans, they tend to meet the acceptance quality criteria less frequently, regardless of the scale of the LLM model.Finally, LLMs can reliably assess the semantic quality of user stories when provided with clear evaluation criteria and have the potential to reduce human effort in large-scale assessments.

A few years after their release, Large Language Models (LLMs)-based tools are becoming an essential component of software education, as calculators are used in math courses. When learning software engineering (SE), the challenge is the extent to which LLMs are suitable and easy to use for different software development tasks. In this paper, we report the findings and lessons learned from using LLM-based tools-ChatGPT in particular-in five SE courses from four universities. After instructing students on the LLM potentials in SE and about prompting strategies, we ask participants to complete a survey and be involved in semi-structured interviews. The collected results report (i) indications about the usefulness of the LLM for different tasks, (ii) challenges to prompt the LLM, i.e., interact with it, (iii) challenges to adapt the generated artifacts to their own needs, and (iv) wishes about some valuable features students would like to see in LLM-based tools. Although results vary among different courses, also because of students' seniority and course goals, the perceived usefulness is greater for lowlevel phases (e.g., coding or debugging/fault localization) than for analysis and design phases. Interaction and code adaptation challenges vary among tasks and are mostly related to the need for task-specific prompts, as well as better specification of the development context.

The accumulation of litter in natural environments poses significant ecological and social challenges, motivating the development of automated solutions for litter detection. However, collecting and centrally aggregating large-scale annotated datasets for training object detectors often raises privacy and ownership concerns. In this work, we propose a Federated Learning (FL) framework to train a lightweight litter detection model based on the YOLO architecture, which enables collaborative model development without requiring centralized access to raw data. Each participating client locally trains the model on site-specific datasets collected in the wild, and only model updates are shared with a central server for aggregation. We compare and contrast different FL process configurations involving mixed and heterogeneous training datasets built starting from two commonly used benchmark datasets collected across different locations and having very different visual data distributions, i.e. TACO and PlastOPol. Experimental results show that the federated model, trained across these non-IID data distributions, achieves superior generalization in cross-dataset evaluation compared to the corresponding centrally trained models.

Simulation-based testing is widely used to assess the reliability of Autonomous Driving Systems (ADS), but its effectiveness is limited by the operational design domain (ODD) conditions available in such simulators. To address this limitation, in this work, we explore the integration of generative artificial intelligence techniques with physics-based simulators to enhance ADS system-level testing. Our study evaluates the effectiveness and computational overhead of three generative strategies based on diffusion models, namely instruction-editing, inpainting, and inpainting with refinement. Specifically, we assess these techniques' capabilities to produce augmented simulator-generated images of driving scenarios representing new ODDs. We employ a novel automated detector for invalid inputs based on semantic segmentation to ensure semantic preservation and realism of the neural generated images. We then performed system-level testing to evaluate the ability of the ADS to generalize to newly synthesized ODDs. Our findings show that diffusion models help to increase the coverage of ODD for system-level ADS testing. Our automated semantic validator achieved a percentage of false positives as low as 3%, retaining the correctness and quality of the images generated for testing. Our approach successfully identified new ADS system failures before real-world testing.

The generation of class integration test orders (CITOs) is a pivotal element in integration testing, which focuses on determining the optimal order for integrating classes while testing an object-oriented system. Due to a high number of dependencies and their possible error proneness, some classes are more critical than others in a program. Existing methods for handling these classes only assess risk in terms of their dependencies; they do not consider historical bug information as an additional indicator and mainly work on small programs. To overcome these limitations, this paper introduces Criticality-Driven CITO (CD-CITO) generation, an innovative approach to optimize CITOs by focusing on class criticality. CD-CITO assesses both the importance of a class in terms of its dependencies and the likelihood of defects, based on historical bug data, to determine a criticality score. Then, it reformulates the CITO generation problem as a Reinforcement learning (RL) task and uses the Advantage Actor-Critic (A2C) algorithm to address it. We propose a novel reward calculation strategy to guide the learning agent, balancing stubbing costs with the criticality values of classes to optimize the test order. To extract fault proneness information and assess the approach, the paper uses Defects4J, a data set that contains real bugs and patches of Java programs. The results obtained show that CD-CITO effectively identifies and prioritizes highly critical classes and also minimizes stubbing costs while generating CITOs, which makes it a valuable tool for integration testing.

Littering is a major problem that threatens the environment, society, and economy. Keep track, monitor and regularly clean littering sites can be a crucial problem that involves public authorities, municipalities, companies, and citizens. So far approaches have not well leveraged the knowledge and capabilities that derive from the federation of multiple communities, such as cities, public bodies, and organizations. In this paper, we describe the COBOL project, a National PRIN (Progetti di Rilevante Interesse Nazionale) PNRR (Piano Nazionale Ripresa e Resilienza) project funded by the Italian MUR (Ministero dell'Università e della Ricerca) in 2023. The project aims to definite a flexible framework for managing the waste disposal process through a federated learning architecture that collects and integrates the reports (e.g., annotated pictures and user feedback) shared by the communities involved in the waste disposal process. To deliver an advanced waste disposal service based on the direct participation of citizens, COBOL also integrates Model-Driven Engineering principles, Computer Vision techniques, and Self-Adaptation mechanisms. Early results show that reports can be effectively collected and processed with COBOL.

Recent breakthroughs in Artificial Intelligence (AI) obfuscate the boundaries between digital, physical, and social spaces, a trend expected to continue in the foreseeable future. Traditionally, software engineering has prioritized technical aspects, focusing on functional correctness and reliability while often neglecting broader societal implications. With the rise of software agents enabled by Large Language Models (LLMs) and capable of emulating human intelligence and perception, there is a growing recognition of the need for addressing socio-critical issues. Unlike technical challenges, these issues cannot be resolved through traditional, deterministic approaches due to their subjective nature and dependence on evolving factors such as culture and demographics. This paper dives into this problem and advocates the need for revising existing engineering principles and methodologies. We propose a conceptual framework for quality assurance where AI is not only the driver of socio-critical systems but also a fundamental tool in their engineering process. Such framework encapsulates pre-production and runtime workflows where LLM-based agents, so-called artificial doppelgängers, continuously assess and refine socio-critical systems ensuring their alignment with established societal standards.

Containerization is a virtualization technique that allows one to create and run executables consistently on any infrastructure. Compared to virtual machines, containers are lighter since they do not bundle a (guest) operating system but they share its kernel, and they only include the files, libraries, and dependencies that are required to properly execute a process. In the past few years, multiple container engines (i.e., tools for configuring, executing, and managing containers) have been developed ranging from some that are “general purpose”, and mostly employed for Cloud executions, to others that are built for specific contexts, namely Internet of Things and High-Performance Computing. Given the importance of this technology for many practitioners and researchers, this paper analyses six state-of-the-art container engines and compares them through a comprehensive study of their characteristics and performance. The results are organized around 0 findings that aim to help the readers understand the differences among the technologies and help them choose the best approach for their needs. Editor’s note: Open Science material was validated by the Journal of Systems and Software Open Science Board.

Applications that are constrained by low-latency requirements can hardly be executed on cloud infrastructures, given the high network delay required to reach remote servers. Multi-access Edge Computing (MEC) is the reference architecture for executing applications on nodes that are located close to users (i.e., at the edge of the network). This way, the network overhead is reduced but new challenges emerge. The resources available on edge nodes are limited, workloads fluctuate since users can rapidly change location, and complex tasks are becoming widespread (e.g., machine learning inference). To address these issues, this article presents NEPTUNE , a serverless-based framework that automates the management of large-scale MEC infrastructures. In particular, NEPTUNE provides (i) the placement of serverless functions on MEC nodes according to users’ location, (ii) the resolution of resource contention scenarios by avoiding that single nodes be saturated, and (iii) the dynamic allocation of CPUs and GPUs to meet foreseen execution times. To assess NEPTUNE , we built a prototype based on K3S, an edge-dedicated version of Kubernetes, and executed a comprehensive set of experiments. Results show that NEPTUNE obtains a significant reduction in terms of response time, network overhead, and resource consumption compared with five state-of-the-art solutions.

Autoscaling systems provide means to automatically change the resources allocated to a software system according to the incoming workload and its actual needs. Public cloud providers offer a variety of autoscaling solutions, ranging from those based on user-written rules to more sophisticated ones. Originally, these solutions were conceived to manage clusters of virtual machines, while more recently, they have also been employed in the operation of containers. This paper analyses the autoscaling solutions provided by three major cloud providers, namely Amazon Web Services, Google Cloud Platform, and Microsoft Azure, and compares them against two solutions we develop based on control theory (ScaleX) and queuing theory (QN-CTRL). We evaluate the different approaches using both an in-house simulation engine and cloud deployments by feeding them with various synthetic and real-world workloads. Our extensive evaluation collects both simulation results and real measurements by which we can assess that both scaleX and QN-CTRL outperform industrial techniques in most cases when considering the trade-offs between the service-level-agreement (SLA) violations and the optimal usage of resources.

Today's technologies are becoming more and more pervasive and advanced software systems can replace human beings in many different tasks. This is especially true in the case of automated decision-making systems based on machine learning (ML). Important ethical implications arise when such decision systems are used in sensitive contexts (e.g., justice or loans). The elicitation of these implications, that is, of the ethical requirements behind ML-based systems is a new challenge we must address to avoid societal risks. This is particularly urgent for fairness since this notion lacks a precise and commonly accepted definition, thus hampering its assessment. This paper aims to give a comprehensive definition of fairness, present a unified taxonomy of alternative interpretations, define a new decision tree that can guide the choice of the correct interpretation, and carry out a preliminary assessment with experiments in a real-world context.

Abstract Cloud computing and virtualization solutions allow one to rent the virtual machines (VMs) needed to run applications on a pay‐per‐use basis, but rented VMs do not offer any guarantee on their performance. Cloud platforms are known to be affected by performance variability , but a better understanding is still required. This article moves in that direction and presents an in‐depth, multi‐faceted study on the performance variability of VMs. Unlike previous studies, our assessment covers a wide range of factors: 16 VM types from 4 well‐known cloud providers, 10 benchmarks, and 28 different metrics. We present four new contributions. First, we introduce a new benchmark suite ( VMBS ) that let researchers and practitioners systematically collect a diverse set of performance data. Second, we present a new indicator, called V I , that allows for measuring variability in the performance of VMs. Third, we illustrate an analysis of the collected data across four different dimensions: resources , isolation , time , and cost . Fourth, we present multiple predictive models based on machine learning (ML) that aim to forecast future performance and detect time patterns. Our experiments provide important insights on the resource variability of VMs, highlighting differences and similarities between various cloud providers. To the best of our knowledge, this is the widest analysis ever conducted on the topic.

The deployment and management of Blockchain applications require non-trivial efforts given the unique characteristics of their infrastructure (i.e., immutability) and the complexity of the software systems being executed. The operation of Blockchain applications is still based on ad-hoc solutions that are error-prone, difficult to maintain and evolve, and do not manage their interactions with other infrastructures (e.g., a Cloud backend).

Nowadays a wide range of applications is constrained by low-latency requirements that cloud infrastructures cannot meet. Multiaccess Edge Computing (MEC) has been proposed as the reference architecture for executing applications closer to users and reducing latency, but new challenges arise: edge nodes are resource-constrained, the workload can vary significantly since users are nomadic, and task complexity is increasing (e.g., machine learning inference). To overcome these problems, the paper presents NEPTUNE, a serverless-based framework for managing complex MEC solutions. NEPTUNE i) places functions on edge nodes according to user locations, ii) avoids the saturation of single nodes, iii) exploits GPUs when available, and iv) allocates resources (CPU cores) dynamically to meet foreseen execution times. A prototype, built on top of K3S, was used to evaluate NEPTUNE on a set of experiments that demonstrate a significant reduction in terms of response time, network overhead, and resource consumption compared to three well-known approaches.

This paper studies how bit-vector logic (bv logic) can help improve the efficiency of verifying specifications expressed in Linear Temporal Logic (LTL). First, it exploits the notion of Bounded Satisfiability Checking to propose an improved encoding of LTL formulae into formulae of bv logic, which can be formally verified by means of Satisfiability Modulo Theories (SMT) solvers. To assess the gain in efficiency, we compare the proposed encoding, implemented in our tool$\mathbb {Z}$ot, against three well-known encodings available in the literature: the classic bounded encoding and the optimized, incremental one, as implemented in both NuSMV and nuXmv, and the encoding optimized for metric temporal logic, which was the “standard” implementation provided by$\mathbb {Z}$ot. We also compared the newly proposed solution against five additional efficient algorithms proposed by nuXmv, which is the state-of-the-art tool for verifying LTL specifications. The experiments show that the new encoding provides significant benefits with respect to existing tools. Since the first set of experiments only used Z3 as SMT solver, we also wanted to assess whether the benefits were induced by the specific solver or were more general. This is why we also embedded different SMT solvers in$\mathbb {Z}$ot. Besides Z3, we also carried out experiments with CVC4, Mathsat, Yices2, and Boolector, and compared the results against the first and second best solutions provided by either NuSMV or nuXmv. Obtained results witness that the benefits of the bv logic encoding are independent of the specific solver. Bv logic-based solutions are better than traditional ones with only a few exceptions. It is also true that there is no particular SMT solver that outperformed the others. Boolector is often the best as for memory usage, while Yices2 and Z3 are often the fastest ones.

Abstract Many software systems today provide support for adaptation and reconfiguration at runtime, in response to changes in their environment. Such adaptive systems are designed to run continuously and may not be shut down for reconfiguration or maintenance tasks. The variability of such systems has to be explicitly managed, together with mechanisms that control their runtime adaptation and reconfiguration. Dynamic software product lines (DSPLs) can help to achieve this. However, dealing with evolution is particularly challenging in a DSPL, as changes made at runtime can easily lead to inconsistencies. This paper describes the challenges of evolving DSPLs using an example cyber‐physical system for home automation. We discuss the shortcomings of existing work and present a reference architecture to support DSPL evolution. To demonstrate its feasibility and flexibility, we implemented the proposed reference architecture for two different DSPLs: the aforementioned cyber‐physical system, which uses feature models to describe its variability, and a runtime monitoring infrastructure, which is based on decision models. To assess the industrial applicability of our approach, we also implemented the reference architecture for a real‐world DSPL, an automation software system for injection molding machines. Our results provide evidence on the flexibility, performance, and industrial applicability of our approach.

Many big-data applications are batch applications that exploit dedicated frameworks to perform massively parallel computations across clusters of machines. The time needed to process the entirety of the inputs represents the application's response time, which can be subject to deadlines. Spark, probably the most famous incarnation of these frameworks today, allocates resources to applications statically at the beginning of the execution and deviations are not managed: to meet the applications' deadlines, resources must be allocated carefully. This paper proposes an extension to Spark, called dynaSpark, that is able to allocate and redistribute resources to applications dynamically to meet deadlines and cope with the execution of unanticipated applications. This work is based on two key enablers: containers, to isolate Spark's parallel executors and allow for the dynamic and fast allocation of resources, and control-theory to govern resource allocation at runtime and obtain required precision and speed. Our evaluation shows that dynaSpark can (i) allocate resources efficiently to execute single applications with respect to set deadlines and (ii) reduce deadline violations (w.r.t. Spark) when executing multiple concurrent applications.

Nowadays software systems are organized around several and heterogeneous components. For example, a modern application can be composed of different microservices, along with dedicated components for machine learning analytics and recurring batch processing jobs. While containers offer a means to deploy the system and tackle heterogeneity, these components have different execution models, can exploit different resource types (e.g., CPUs and GPUs) and result in completely different execution times (milliseconds vs hours). This complexity calls for a new, scalable architecture to allow the systems to operate efficiently. This paper presents COCOS, an architecture, based on containers and control-theory, that is able to manage large and heterogeneous software systems. The architecture is based on a three-level hierarchy of controllers that cooperatively enforce user-defined requirements on execution times and consumed resources. The paper also shows a prototype implementation of COCOS based on Kubernetes, a well-known container orchestrator. The evaluation shows the efficiency of COCOS when dealing with microservices, Spark jobs and machine learning applications.

Dynamic resource allocation is the mechanism that allows one to change the resources associated with applications at runtime and match their actual needs. The autoscaling solutions offered by cloud infrastructures are probably the most widely-used incarnation of this concepts. Originally conceived to manage virtual machines according to user-defined rules, they are now much more sophisticated and can also allocate containers (lighter than virtual machines). This paper surveys the autoscaling solutions provided by the major cloud vendors and analyzes the services they provide. It also compares them against the solution we developed, called COCOS autoscaling. We simulated the different proposals and fed them with diverse workloads. Obtained results show that COCOS autoscaling outperforms its competitors in most of the cases: it optimizes resource allocation and keeps applications' response times under set thresholds.

Abstract Apache Spark is probably the most widely adopted framework for developing big-data batch applications and for executing them on a cluster of (virtual) machines. In general, the more resources (machines) one uses, the faster applications execute, but there is currently no adequate means to determine the proper size of a Spark cluster given time constraints, or to foresee execution times given the number of employed machines. One can only run these applications and use her/his experience to size the cluster and predict expected execution times. Wrong estimation of execution times can lead to costly overruns and overly long executions, thus calling for analytic sizing/prediction techniques that provide precise time guarantees. This paper addresses this problem by proposing a solution based on model-checking. The approach exploits a directed acyclic graph (DAG) to abstract the structure of the execution flows of Spark programs, annotates each node (Spark stage) with execution-related data, and formulates the identification of the global execution time as a reachability problem. To avoid the well-known state space explosion problem, the paper also proposes a technique to reduce the size of generated abstract models. This results in a significant decrease in used memory and/or verification time making our approach feasible for predicting the execution time of Spark applications given the resources available. The benefits of the proposed reduction technique are evaluated by using both timed automata and constraint LTL over clocks logic to formally encode and analyze generated models. The approach is also successfully validated on some realistic case studies. Since the optimization is not Spark-specific, we claim that it can be applied to a wide range of applications whose underlying model can be abstracted as a DAG.

Internet-enabled devices operating in the physical world are increasingly integrated in modern distributed systems. We focus on systems where the dynamics of spatial distribution is crucial; in such cases, devices may need to carry out complex computations (e.g., analyses) to check satisfaction of spatial requirements. The requirements are partly global—as the overall system should achieve certain goals—and partly individual, as each entity may have different goals. Assurance may be achieved by keeping a model of the system at runtime, monitoring events that lead to changes in the spatial environment, and performing requirements analysis. However, computationally intensive runtime spatial analysis cannot be supported by resource-constrained devices and may be offloaded to the cloud. In such a scenario, multiple challenges arise regarding resource allocation, cost, performance, among other dimensions. In particular, when the workload is unknown at the system’s design time, it may be difficult to guarantee application-service-level agreements, e.g., on response times. To address and reason on these challenges, we first instantiate complex computations as microservices and integrate them to an IoT-cloud architecture. Then, we propose alternative cloud deployments for such an architecture—based on virtual machines, containers, and the recent Functions-as-a-Service paradigm. Finally, we assess the feasibility and tradeoffs of the different deployments in terms of scalability, performance, cost, resource utilization, and more. We adopt a workload scenario from a known dataset of taxis roaming in Beijing, and we derive other workloads to represent unexpected request peaks and troughs. The approach may be replicated in the design process of similar classes of spatially distributed IoT systems.

The execution of Spark applications is based on the execution order and parallelism of the different jobs, given data and available resources. Spark reifies these dependencies in a graph that we refer to as the (parallel) execution plan of the application. All the approaches that have studied the estimation of the execution times and the dynamic provisioning of resources for this kind of applications have always assumed that the execution plan is unique, given the computing resources at hand. This assumption is at least simplistic for applications that include conditional branches or loops and limits the precision of the prediction techniques.

Technologies such as mobile, edge, and cloud computing have the potential to form a computing continuum for new, disruptive applications. At runtime, applications can choose to execute parts of their logic on different infrastructures that constitute the continuum, with the goal of minimizing latency and battery consumption and maximizing availability. In this article, we propose A3-E, a unified model for managing the life cycle of continuum applications. In particular, A3-E exploits the Functions-as-a-Service model to bring computation to the continuum in the form of microservices. Furthermore, A3-E selects where to execute a certain function based on the specific context and user requirements. The article also presents a prototype framework that implements the concepts behind A3-E. Results show that A3-E is capable of dynamically deploying microservices and routing the application’s requests, reducing latency by up to 90% when using edge instead of cloud resources, and battery consumption by 74% when computation has been offloaded.

This extended abstract summarizes our paper entitled "A Comparison Framework for Runtime Monitoring Approaches" published in the Journal on Systems and Software in vol. 125 in 2017 (https://doi.org/10.1016/jjss.2016.12.034). This paper provides the following contributions: (i) a framework that supports analyzing and comparing runtime monitoring approaches using different dimensions and elements; (ii) an application of the framework to analyze and compare 32 existing monitoring approaches; and (iii) a discussion of perspectives and potential future applications of our framework, e.g., to support the selection of an approach for a particular monitoring problem or application context.

This paper presents MAGNET, a novel middleware infrastructure that exploits Wi-Fi Direct to provide a reliable and stable communication means for large numbers of mobile devices. This self-organizing middleware abstracts the multi-hop communication process by autonomously maintaining connectivity among devices. MAGNET also provides a discovery mechanism that exploits the MAC address of the different devices or the services they offer. MAGNET was evaluated both on our WiDiSi simulator for Wi-Fi Direct-based systems, and on real Android devices. The results we obtained in our evaluation illustrate the effectiveness of the proposed middleware, both in discovering and maintaining connectivity in large-scale dynamic scenarios.

This article presents a novel technique to formally verify models of real-time systems captured through a set of heterogeneous UML diagrams. The technique is based on the following key elements: (i) a subset of Unified Modeling Language (UML) diagrams, called Coretto UML (C-UML), which allows designers to describe the components of the system and their behavior through several kinds of diagrams (e.g., state machine diagrams, sequence diagrams, activity diagrams, interaction overview diagrams), and stereotypes taken from the UML Profile for Modeling and Analysis of Real-Time and Embedded Systems; (ii) a formal semantics of C-UML diagrams, defined through formulae of the metric temporal logic Tempo Reale ImplicitO (TRIO); and (iii) a tool, called Corretto, which implements the aforementioned semantics and allows users to carry out formal verification tasks on modeled systems. We validate the feasibility of our approach through a set of different case studies, taken from both the academic and the industrial domain.

Modern component-based distributed software systems are increasingly required to offer non-stop service and thus their updates must be carried out at runtime. Different authors have already proposed solutions for the safe management of dynamic updates. Our contribution aims at improving their efficiency without compromising safety. We propose a new criterion, called version consistency, which defines when a dynamic update can be safely and efficiently applied to the components that execute distributed transactions. Version consistency ensures that distributed transactions be served as if they were operated on a single coherent version of the system despite possible concurrent updates. The paper presents a distributed algorithm for checking version consistency efficiently, formalizes the proposed approach by means of a graph transformation system, and verifies its correctness through model checking. The paper also presents ConUp, a novel prototype framework that supports the approach and offers a viable, concrete solution for the use of version consistency. Both the approach and ConUp are evaluated on a significant third-party application. Obtained results witness the benefits of the proposed solution with respect to both timeliness and disruption.

Modern Web applications exploit Cloud infrastructures to scale their resources and cope with sudden changes in the workload. While the state of practice is to focus on dynamically adding and removing virtual machines, we advocate that there are strong benefits in containerizing the applications and in scaling the containers.

This paper describes WiDiSi, a research-oriented prototype simulator for Wi-Fi Direct networks. WiDiSi is provided as an extension of PeerSim, a widely-used, open-source simulation framework for large-scale peer to peer networks. WiDiSi's main goal is to allow Android Wi-Fi direct applications to be easily tested in large-scale dynamic scenarios. In this article, we explain how WiDiSi was modeled and present its general architecture. We also provide evaluation results that show the correctness and the capabilities of the simulator.

Smart interconnected devices are changing our lives and are turning conventional spaces into smart ones. Physical proximity, a key enabler of social interactions in the old days is not exploited by smart solutions, where the social dimension is always managed through the Internet. This paper aims to blend the two forces and proposes the idea of social smart space, where modern technologies can help regain and renew social interactions, and where proximity is seen as enabler for dedicated and customized functionality provided by users to users. A Social Proximity Framework (SPF) provides the basis for the creation of this new flavor of smart spaces. Two different versions of the SPF, based on different communication infrastructures, help explain the characteristics of the different components, and show how the SPF can benefit from emerging connection-less communication protocols. A first assessment of the two implementations concludes the paper.

Linear Temporal Logic (LTL) has been used in computer science for decades to formally specify programs, systems, desired properties, and relevant behaviors. This paper presents a novel, efficient technique for verifying LTL specifications in a fully automated way. Our technique belongs to the category of Bounded Satisfiability Checking approaches, where LTL formulae are encoded as formulae of another decidable logic that can be solved through modern satisfiability solvers. The target logic in our approach is Bit-Vector Logic. We present our novel encoding, show its correctness, and experimentally compare it against existing encodings implemented in well-known formal verification tools.

Big Data is about extracting valuable information from data in order to use it in intelligent ways such as to revolutionize decision-making in businesses, science and society. BIGDSE 2015 discusses the link between Big Data and software engineering and critically looks into issues such as cost-benefit of big data.

In many domains systems need to run continuously and cannot be shut down for reconfiguration or maintenance tasks. Cyber-physical or cloud-based systems, for instance, thus often provide means to support their adaptation at runtime. The required flexibility and adaptability of systems suggests the application of Software Product Line (spl) principles to manage their variability and to support their reconfiguration. Specifically, Dynamic Software Product Lines (dspl) have been proposed to support the management and binding of variability at runtime. While spl evolution has been widely studied, it has so far not been investigated in detail in a dspl context. Variability models that are used in a dspl have to co-evolve and be kept consistent with the systems they represent to support reconfiguration even after changes to the systems at runtime. In this short paper we present a classification of the required operations for jointly evolving problem and solution space in a dspl. We analyze the impact of such operations on the consistency of a dspl and propose an approach to deal with the described issues. We describe a runtime monitoring system used in the domain of industrial automation software as an example of a dspl evolving at runtime to motivate and explain our work.

Self-adaptive systems, services, and product lines can be seen as different facets of the same problem. Self-adaptation provides the requirements, product lines a conceptual means to frame them, and services a possible technology to implement the resulting systems. This short paper starts presenting an overview of the many solutions proposed for adding self-adaptive capabilities to software systems. It also introduces service-based solutions and software product lines to discuss what self-adaptive systems can borrow from them.

Service-based business processes must evolve to remain aligned with their goals, with zero downtime to guarantee business continuity. A new version of a service should be adopted as soon as it becomes available to let clients benefit from the updated functionality and/or improved quality of service. In practice, however, existing services may be involved in distributed computations that cannot immediately adopt the new versions without suffering inconsistencies. The paper proposes a solution for the consistent runtime evolution of service-based business processes: new service versions can be adopted safely and in a timely fashion, and old versions can be consistently decommissioned. The proposal has been evaluated in the context of an online bank wire transfer example. Our experiments show that the approach is timely in activating service updates, and that the overhead it introduces is negligible.

No abstract available.

Due to the growing pervasiveness of the service paradigm, modern systems are now often built as software as a service, and tend to exploit underlying platforms and virtualized resources also provided as services. Managing such systems requires that we be aware of the behaviors of all the different layers, and of the strong dependencies that exist between them. In this paper we present the Multi-layer Collection and Constraint Language (mlCCL). It allows us to define how to collect, aggregate, and analyze runtime data in a multi-layered system. We also present ECoWare, a framework for event correlation and aggregation that supports mlCCL, and provides a dashboard for on-line and off-line drill-down analyses of collected data. Empirical assessment shows that the impact of the approach on runtime performance is negligible.

This paper describes IRENE (Indenica Requirements ElicitatioN mEthod), a methodology to elicit and model the requirements of service platforms, and IRET (IREne Tool), the Eclipse-based modeling framework we developed for IRENE.

This paper presents a partially-automated solution for the definition of test oracles for validating Simulink models. Since these models are widely used for the design of embedded systems, their thorough validation is key. Errors and misunderstandings in these models may preclude the correctness and reliability of the final system: a manual, human-intensive validation activity is not enough, and automated solutions are fundamental to improve the current state of the art. The paper also presents Apolom, a prototype oracle generator, and the results of two experiments.

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.

The design of complex embedded software systems requires the careful analysis of the system and of the environment it interacts with. The different natures of these two elements are difficult to address by means of a single all-encompassing technique/notation. The paper proposes MCA, the MADES Co-simulation Approach, which allows designers to combine different, complementary formalisms in a seamless manner: the system is rendered through logic formulae, while the environment is demanded to Modelica. These two models are input to MCA to produce an execution trace that is “compatible” with them, that is, that does not violate either model. The paper introduces the theoretical basis of MCA and exemplifies it on a case study.

This workshop on services, clouds, and alternative design strategies for variant-rich software systems brings together researchers and practitioners that are interested in or have been working on variant-rich software systems.

The modernization of a software system is a complex and expensive task and requires a deep understanding of the existing system. The capability of re-factoring a complex application into some high-level views is mandatory to elicit its structure and start localize possible changes. The high number of different implementation technologies imposes a model-based, neutral approach to reconstruct the structure and hide unnecessary details. OMG supports this view and proposes KDM (Knowledge Discovery Meta model) as means to describe software systems in detail, but unfortunately KDM supports a component-oriented decomposition of the system of interest only partially. To bypass this limitation, the paper proposes the COMO (Component-Oriented MOdernization) meta model to extend KDM, by borrowing recurring concepts from component-based solutions and software architectures, and to support a proper componentization of the system we want to modernize. The paper presents the main elements of the COMO meta model and exemplifies them on a simple case study.

There is an increasing demand for the runtime reconfiguration of distributed systems in response to changing environments and evolving requirements. Reconfiguration must be done in a safe and low-disruptive way. In this paper, we propose version consistency of distributed transactions as a safe criterion for dynamic reconfiguration. Version consistency ensures that distributed transactions be served as if there were operating on a single coherent version of the system despite possible reconfigurations that may happen meanwhile. The paper also proposes a distributed algorithm to maintain dynamic dependences between components at architectural level and enable low-disruptive version-consistent dynamic reconfigurations. An initial assessment through simulation shows the benefits of the proposed approach with respect to timeliness and low degree of disruption.

Summary of Scarves workshop

Distributed systems comprise a significant number of entities that must be properly coordinated to reach a goal. These systems present high turnover of elements, and demand for solutions that keep their coordination as decentralized as possible to avoid bottlenecks. The paper discusses why it is important to address these characteristics from a system's conception and proposes A-3, an innovative architectural solution that adopts the concept of group as an abstraction for organizing an application into semi-independent slices, providing a single and coherent view of these aggregates, and coordinating the interactions inside and among groups. The paper presents the A-3 model and defines it as an innovative architectural style, describes a Java-based framework that supports A-3 and provides users with the proper means to exploit the style, and exemplifies all the main concepts on a simple scenario where autonomous robotic vacuum cleaners are coordinated to properly clean a museum.

Service compositions suffer changes in their partner services. Even if the composition does not change, its behavior may evolve over time and become incorrect. Such changes cannot be fully foreseen through prerelease validation, but impose a shift in the quality assessment activities. Provided functionality and quality of service must be continuously probed while the application executes, and the application itself must be able to take corrective actions to preserve its dependability and robustness. We propose the idea of self-supervising BPEL processes, that is, special-purpose compositions that assess their behavior and react through user-defined rules. Supervision consists of monitoring and recovery. The former checks the system's execution to see whether everything is proceeding as planned, while the latter attempts to fix any anomalies. The paper introduces two languages for defining monitoring and recovery and explains how to use them to enrich BPEL processes with self-supervision capabilities. Supervision is treated as a cross-cutting concern that is only blended at runtime, allowing different stakeholders to adopt different strategies with no impact on the actual business logic. The paper also presents a supervision-aware runtime framework for executing the enriched processes, and briefly discusses the results of in-lab experiments and of a first evaluation with industrial partners.

The Publish-Subscribe (P/S) communication paradigm fosters high decoupling among distributed components. This facilitates the design of dynamic applications, but also impacts negatively on their verification, making it difficult to reason on the overall federation of components. In addition, existing P/S infrastructures offer radically different features to the applications, e.g., in terms of message reliability. This further complicates the verification as its outcome depends on the specific guarantees provided by the underlying P/S system. Although model checking has been proposed as a tool for the verification of P/S architectures, existing solutions overlook many characteristics of the underlying communication infrastructure to avoid state explosion problems. To overcome these limitations, the Loupe domain-specific model checker adopts a different approach. The P/S infrastructure is not modeled on top of a general-purpose model checker. Instead, it is embedded within the checking engine, and the traditional P/S operations become part of the modeling language. In this paper, we describe Loupe's design and the dedicated state abstractions that enable accurate verification without incurring state explosion problems. We also illustrate our use of state-of-the-art software verification tools to assess some key functionality in Loupe's current implementation. A complete case study shows how Loupe eases the verification of P/S architectures. Finally, we quantitatively compare Loupe's performance against alternative approaches. The results indicate that Loupe is effective and efficient in enabling accurate verification of P/S architectures.

TestFul is a novel evolutionary testing approach for object-oriented programs with complex internal states. In our preliminary experiments, it already outperformed some of the well-known search-based testing approaches. In this paper we show how TestFul can be further improved by leveraging three efficiency enhancement techniques: seeding, hybridization, and fitness inheritance. We considered four extensions of TestFul: three using each enhancement separately, and one using all of them at the same time. We used these new versions of TestFul to generate tests for six Java classes taken from the literature, public software libraries, and third party benchmarks. We compared the performance of the original TestFul against these new versions. Our results show that each enhancement technique results in a significant speed-up and, even more interesting, the highest improvement is achieved when all the enhancements are combined together.

This paper presents TestFul , an Eclipse plugin for the generation of tests for Java classes. It is based on the idea of search-based testing, working both at class and method level. The former puts objects in useful states, used by the latter to exercise the uncovered parts of the class.

This paper presents TestFul, an evolutionary testing approach for Java classes that works both at class and method level. TestFul exploits a multi-objective evolutionary algorithm to identify the “best” tests. The paper introduces the main elements of TestFul. It also compares TestFul against well-known search-based solutions using a set of classes taken from literature, known software libraries, and independent testing benchmarks. The comparison considers statement and branch coverage, size of generated tests, and generation time. On considered classes, TestFul generates better tests than other search-based solutions, and achieves higher structural coverages with tests small enough to be usable.

Service compositions need to continuously self- adapt to cope with unexpected failures. In this context adaptation becomes a fundamental requirement that must be elicited along with the other functional and non functional requirements. Beside modelling, effective adaptation also demands means to trigger it at runtime as soon as the actual behavior of the composition deviates from stated requirements. This paper extends traditional goal models with adaptive goals to support continuous adaptation. Goals become live, runtime entities whose satisfaction level is dynamically updated. Furthermore, boundary infringement triggers adaptation capabilities. The paper also provides a methodology to trace goals onto the underlying composition, assess goals satisfaction at runtime, and activate adaptation consequently. All the key elements are demonstrated on the definition of the process to control an advanced washing machine.

Self-adaptation is imposing as a key characteristic of many modern software systems to tackle their complexity and cope with the many environments in which they can operate. Self-adaptation is a requirement per-se, but it also impacts the other (conventional) requirements of the system; all these new and old requirements must be elicited and represented in a coherent and homogenous way. This paper presents FLAGS, an innovative goal model that generalizes the KAOS model, adds adaptive goals to embed adaptation countermeasures, and fosters self-adaptation by considering requirements as live, runtime entities. FLAGS also distinguishes between crisp goals, whose satisfaction is boolean, and fuzzy goals, whose satisfaction is represented through fuzzy constraints. Adaptation countermeasures are triggered by violated goals and the goal model is modified accordingly to maintain a coherent view of the system and enforce adaptation directives on the running system. The main elements of the approach are demonstrated through an example application.

This paper introduces TestFul, a framework for testing stateful systems and focuses on object-oriented software. TestFul employs a hybrid multi-objective evolutionary algorithm, to explore the space of feasible tests efficiently, and novel quality metrics, based on both def-use pairs and behavioral coverage, to judge the quality of tests. We compare our framework against random testing by considering the level of coverage, the size of generated tests, and the time required to generate the tests. Our preliminary results show the validity of the approach: TestFul outperforms random testing in most of the cases.

In the literature, there exist several approaches for monitoring the execution of BPEL processes. They concentrate on different properties, adopt different languages, work at different levels of abstraction, and assume different perspectives. Even if the field is rather new, we do not think that this diversity is a limitation of current solutions; rather it is intrinsic in the problem itself. We claim that, instead of working on the definition of the ultimate approach for BPEL monitoring, we should push a cooperative approach based on the integration of different solutions.In this paper, we present a first step in this direction, and describe a monitoring framework which is obtained by integrating two well-known approaches, namely Dynamo and Astro. This integration, which happens both for the language used for expressing the properties to be monitored, and for the architecture of the monitoring framework, allows to combine the advantages of the two approaches and to obtain a general, comprehensive solutions for BPEL monitoring.

This mini-tutorial introduces Web services and service-centric systems, identifies their impact on requirements engineering, and introduces new tools and techniques for engineer requirements for service-centric systems.

The paper presents a novel approach based on Bogor for the accurate verification of applications based on Publish- Subscribe infrastructures. Previous efforts adopted standard model checking techniques to verify the application behavior, but they introduce strong simplifications on the underlying infrastructure to cope with the state space explosion problem and make automatic verification feasible. Instead of building on top of existing model checkers, our proposal embeds the asynchronous communication mechanisms of Publish-Subscribe infrastructures within Bogor. This way, Publish-Subscribe primitives become part of the specification language as additional, domain-specific, constructs. Accurate models become feasible without incurring in state space explosion problems, thus enabling the automated verification of applications on top of realistic communication infrastructures.

Web service based applications are expected to live in dynamically evolving settings. At run-time, services may undergo changes that could modify their expected behavior. Because of such intrinsic dynamic nature, applications should be designed by adhering to the principles of design- by-contract. Run-time monitoring is needed to check that the contract between service providers and service users is fulfilled while the collaboration is in place. We describe a language to specify the expected functional and non-functional requirements that a service provider should fulfill. The language (timed WSCoL) is a temporal extension of a previous proposal (WSCoL). We also illustrate the architecture of a run-time analyzer that checks timed WSCoL properties. Should such properties be disproved during execution, appropriate recovery and reconfiguration actions may be put in place.

Our research focuses on the effort needed for designing modern Web applications. The design effort is an important part of the total development effort, since the implementation can be partially automated by tools. We carried out three empirical studies with students of advanced university classes enrolled in engineering and communication sciences curricula. The empirical studies are based on the use of W2000, a special-purpose design notation for the design of Web applications, but the hypotheses and results may apply to a wider class of modeling notations (e.g., OOHDM, WebML, or UWE). We started by investigating the relative importance of each design activity. We then assessed the accuracy of a priori design effort predictions and the influence of a few process-related factors on the effort needed for each design activity. We also analyzed the impact of attributes like the size and complexity of W2000 design artifacts on the total effort needed to design the user experience of web applications. In addition, we carried out a finer-grain analysis, by studying which of these attributes impact the effort devoted to the steps of the design phase that are followed when using W2000.

The increasing diffusion of ubiquitous communication infrastructures and physical active objects-like sensors and smart tags-is motivating the integration of these devices into advanced distributed systems. The novelty of these technologies has imposed a "code and fix" approach; only a few methodologies have been developed to address the integration of heterogeneous technologies to provide the user with sophisticated and flexible abstractions of real world objects. To this end, the paper proposes the first results of a model-driven approach for the development of applications based on heterogeneous physical active objects. We propose a metamodel and a framework for automatic code generation based on Jini. The approach is exemplified on a simple case study in the domain of advanced logistics.

This tutorial introduces dynamic web services as a solution to cope with the dynamism and flexibility required by many modern software systems. Current technologies (WSDL, WS-BPEL, etc.) have proven insufficient in addressing these issues; however, they remain a good starting point for the analysis of the current situation and for building for the future.The core part of the tutorial analyzes ---by looking at available technologies and prominent research proposals---the deployment and execution of these applications within three separate phases: a composition phase, to discover available services and implement the desired behavior, a monitoring phase, to understand if a given service is behaving correctly (with respect to both functional and non-functional requirements), and a recovery phase, to react to anomalies by means of suitable replanning or recovery strategies.In conclusion, the tutorial summarizes the main topics, presents a list of still-to-be-solved problems, and highlights possible directions for future research.

Summary form only given. Traditional software development is based on the closed-world assumption that the boundary between system and environment is known and unchanging. However, this assumption no longer works within today's unpredictable open-world settings, which demands techniques that let software react to changes by self-organizing its structure and self-adapting its behavior

The service-oriented approach is becoming more and more popular to integrate highly heterogeneous systems. Service-oriented architectures (SoAs) define a new flexible coordination paradigm for integrating components (services) in unstable and evolving contexts, where the high degree of flexibility and dynamism requires that available functionality be discovered at run-time and its quality parameters be negotiated dynamically. This is the case, for example, of ambient computing and automotive applications that need to cope with continuously evolving configurations. The dynamic nature of these systems precludes the a-priori identification of the components that define the system and demands for the run-time discovery and composition of such services, adding uncertainty to the system. It could be the case, for example, that a binding (request/provision) cannot span multiple executions since the changing context alters the set of available services. This means that problems related to the discovery of services should also be considered and handled at run-time. If the selection phase aborts, simply shutting down the system is not, in general, going to be a solution. The execution environment should be able to select new services and even reorganize the process to find a solution that uses what is available, if a perfect match does not exist.

The article proposes an approach for defining extensible and flexible formal interpreters for diagram notations with significant dynamic semantics. More precisely, it addresses semi-formal diagram notations that have precisely-defined syntax, but informally defined (dynamic) semantics. These notations are often flexible to fit the different needs and expectations of users. Flexibility comes from the incompleteness or informality of the original definition and results in different interpretations.The approach defines interpreters by means of a mapping onto a semantic domain. Two sets of rules define the correspondences between the elements of the diagram notation and those of the semantic domain, and between events and states of the semantic domain and visual annotations on the elements of the diagram notation.Flexibility also leads to notation families, that is, sets of notations that share core concepts, but present slightly different interpretations. Existing approaches usually interpret these notations in isolation; the approach presented in this article allows the interpretation of a family as a whole. The feasibility of the approach is demonstrated through a prototype generator that allows users to implement special-purpose interpreters by defining relatively small sets of rules.

Service-based approaches are widely used to integrate heterogenous systems. Web services allow for the definition of highly dynamic systems where components (services) can be discovered and QoS parameters negotiated at run-time. This justifies the need for monitoring service compositions at run-time. Research on this issue, however, is still in its infancy.

In this paper, we address the correct refinement of abstract architectural models into more platform-specific representations. We consider the challenging case of dynamic architectures which can perform run-time reconfigurations. For this purpose, the underlying platform has to provide the necessary reconfiguration mechanisms. To conceptually model such platforms including provided reconfiguration mechanisms, we use architectural styles formalized by graph transformation rules. Based on formal refinement relations between abstract and platform-specific styles, we can then investigate how to realize business-specific scenarios on a certain platform by automatically deriving refined, platform-specific reconfiguration scenarios.

Most applications developed today rely on a given middleware platform which governs the interaction between components, the access to resources, etc. To decide, which platform is suitable for a given application (or more generally, to understand the interaction between application and platform), we propose UML models of both the architectural style of the platform and the application scenario. Based on a formal interpretation of these as graphs and graph transformation systems, we are able to validate the consistency between platform and application.

Modern Web applications are mainly distributed systems that exploit the Internet as communication means and the Web as neutral interface to access services and data. The addition of services to Web applications poses problems that are usually tackled at the technology level, but that should be addressed during design to deliver quality Web applications. A typical example of these problems is the Amazon bug, an annoying problem that the user could encounter if after adding products to his shopping cart, he rolls back to a page with a previous version of the cart and tries to buy it. This would make the user buy the last version of the cart's contents, which in some subtle cases could be different from what expected.In this paper, we do not want to discuss all design aspects, but only how provided services/operations should jointly be designed with the rest of the system. We propose a new reference model for Web applications: Operations require a more complex model where they are not simply appended to information and navigation elements, but they can cooperate with them. Besides the reference model, the paper proposes the use of assertions to constraint the behavior of designed operations. Assertions do not only predicate on how data should be modified, but must also take into account how presentation and navigation could be affected by the execution of the operation.

We study the effort needed for designing Web applications from an empirical point of view. The design phase forms an important part of the overall effort needed to develop a Web application, since the use of tools can help automate the implementation phase. We carried out an empirical study with students of an advanced university class that used W2000 as a Web application design technique. Our first goal was to compare the relative importance of each design activity. Second, we tried to assess the accuracy of a priori design effort predictions and the influence of factors on the effort needed for each design activity. Third, we also studied the quality of the designs obtained.

Strong timing requirements and complex interactions with controlled elements complicate the design and validation of software controllers. Different techniques have been proposed to cope with these problems during the different development steps: for example, differential equations for modeling controlled elements, the IEC 1131-3 notations for designing the software controller, and formal models for validating the design, but no definitive solutions have been proposed yet. The paper describes PLCTOOLS, a toolbox that exploits all the aforementioned techniques to supply an integrated environment for the design, formal validation, and automatic code generation of software controllers.

Real-time extensions to structured analysis (SA/RT) are popular in industrial practice. Despite the large industrial experience and the attempts to formalize the various “dialects,” SA/RT notations are still imprecise and ambiguous. This article tries to identify the semantic problems of the requirements definition notation defined by Hatley and Pirbhai, one of the popular SA/RT “dialects,” and discusses possible solutions. As opposed to other articles that give their own interpretation, this article does not propose a specific semantics for the notation. This article identifies imprecisions, i.e., missing or partial information about features of the notation; it discusses ambiguities, i.e., elements of the definition that allow at least two different (“reasonable”) interpretations of features of the notation; and it lists extensions, i.e., features not belonging to the notation, but required by many industrial users and often supported by CASE tools. This article contributes by clarifying whether specific interpretations can be given unique semantics or retain ambiguities of the original definition. The article allows for the evaluation of formal definitions by indicating alternatives and consequences of the specific choices.

Health care systems are becoming extremely complex and expensive. New methods are required to optimize health care processes in order to guarantee high quality standards within the (limited) available resources. Resource optimizations able to preserve the quality of treatments require good models of diagnostic and therapeutic processes. This paper proposes LEMMA, a new model for medical processes, that mixes formal and informal notations, overcoming the problems of either approaches. LEMMA merges highly expressive specific constructs with a formal definition. LEMMA has been validated using a prototype for modeling and analyzing diagnostic processes.

Formal specification methods are not often applied in industrial projects, despite their advantages and the maturity of theories and tools.The scarce familiarity of practitioners with formal notations and the difficulties of their use are main causes of the limited success of formal specification methods.Approaches based on the use of popular front-end notations formally defined with mappings on formal models can solve practical problems.However the absence of flexibility of the mappings proposed so far limits the applicability of such approaches to the few environments that match exactly these solutions.This paper presents an original solution based on formalisms to define mappings from front-end notations to formal models.The proposed framework works with different front-end notations and formal models and supports mappings of analysis results obtained on the formal model to the front-end notation chosen by the practitioners.The approach described in this paper has been validated in industrial environments using pilot applications.The paper presents some of the industrial results obtained so far and ongoing experimentations.

Rigorous formal methods and intuitive graphical notations can greatly enhance the development of complex computer systems. Formal methods guarantee non-ambiguity and support powerful analysis techniques. Intuitive graphical notations facilitate the communications between engineers preventing errors due to misunderstandings. Unfortunately, tools and techniques based on formal methods do not usually support adequate graphical notations; while tools and methods based on powerful graphical notations often lack formal foundations. This paper proposes a technique that allows kernel formalisms to be accessed through powerful graphical notations. The proposed technique allows graphical notations to be tailored to the needs of the specific application domain. This paper focuses on the tool support.