Abstract We present a tool for the compositional verification and correct-by-construction synthesis of stochastic world models —heterogeneous networks of interdependent stochastic models including discrete and continuous-time Markov chains, Markov decision processes (MDPs), partially observable MDPs, and stochastic multi-player games. Through its unique integration of multiple probabilistic and parametric model checking paradigms, our tool unifies the modelling, verification and synthesis of systems characterised by a combination of probabilistic and nondeterministic uncertainty, discrete and continuous-time behaviour, partial observability, and multi-agent interaction.

AI at the network edge promises real-time perception and decision-making in safety-critical domains such as aerial robotics, autonomous vehicles, and 5G-enabled infrastructures. Yet, operating under resource constraints, dynamic, and adversarial conditions exposes edge AI systems to fragility, inefficiency, and security risks that threaten their safe operation. GuardAI, a Horizon Europe project, introduces a framework for resilient and trustworthy edge AI that unites three pillars: adversarial robustness, context-enhanced inference, and security-by-design. Initial project results include a diffusion-based adversarial purification framework optimized for real-time operation, lightweight deep unrolling architectures for LiDAR super-resolution with built-in outlier removal, and robust uncertainty quantification modules to improve confidence calibration. It further develops a context-enhanced inference engine that integrates visual, spatial, and operational context across multi-agent systems, and a risk-aware defense recommender that autonomously selects mitigation strategies based on evolving threat landscapes. Through representative Use Cases, covering monitoring with Unmanned Aerial Vehicle, decentralized 5G network analytics, and secure perception in connected autonomous vehicles, GuardAI demonstrates how robust and adaptive AI can be achieved within stringent edge constraints. Together, these technologies lay the groundwork for a new generation of secure, context-aware, and certifiable AI systems that can be trusted to operate autonomously in the physical world.

Unmanned Aerial Vehicles (UAVs) have become essential in search and rescue operations, especially in disaster management scenarios. Their effective navigation and the integration of a plethora of sensors assist in efficient person detection, making them an essential technological tool to first responders. Multi-UAV systems extend these benefits by using coordinated strategies to cover large areas efficiently, reducing overall mission response time and enhancing its success. Despite these advantages, challenges remain in ensuring the safety, security, and dependability of (mutli-)UAV missions. Issues such as navigation risks, potential cyber threats, and hardware-/software-related reliability issues can impact the mission results. Additionally, UAVs are highly constrained devices with limited battery capacity, requiring the use of lightweight technologies. In this paper, we present part of the results of the SESAME project, an EU multi-partner project that aims to develop safe and secure multi-robot Systems. In particular, we present some of the developed SESAME Executable Digital Dependability Identities (EDDI) technologies based on Markov models, statistical distance measures, and other advanced approaches for enhancing safety, security and dependability of the UAV platform and underlying models. These EDDI technologies are seamlessly integrated using the ConSerts framework in a multi-UAV platform and tested using search and rescue scenarios. The results demonstrate significant improvements in multi-UAV safety, with an availability rate of 91% and a search and rescue algorithmic accuracy of 99.8%. Additionally, the system achieves precise detection of spoofing attacks, using collaborative localization as a mitigation technique to guide the UAV to a safe landing, even in the absence of GPS signals,

Safe exploration of reinforcement learning (RL) agents is a critical activity for empowering their deployment in many real-world scenarios. When prior knowledge of the target domain or task is unavailable, training RL agents in unknown, black-box environments unavoidably yields significant safety risks. Our ADVICE (Adaptive Shielding with a Contrastive Autoencoder) novel post-shielding approach operates in continuous state and action spaces, distinguishing safe and unsafe features of state-action pairs during training, and uses this knowledge to safeguard the RL agent from executing actions that yield likely hazardous outcomes. Our comprehensive experimental evaluation shows that ADVICE significantly reduces safety violations (≈50%) compared to state-of-the-art safe RL exploration approaches, while maintaining a competitive outcome reward for the synthesised safe policy.

Quantifying uncertainty in deep regression models is important both for understanding the confidence of the model and for safe decision-making in high-risk domains. Existing approaches that yield prediction intervals overlook distributional information, neglecting the effect of multimodal or asymmetric distributions on decision-making. Similarly, full or approximated Bayesian methods, while yielding the predictive posterior density, demand major modifications to the model architecture and retraining. We introduce MCNF, a novel post hoc uncertainty quantification method that produces both prediction intervals and the full conditioned predictive distribution. MCNF operates on top of the underlying trained predictive model; thus, no predictive model retraining is needed. We provide experimental evidence that the MCNF-based uncertainty estimate is well calibrated, is competitive with state-of-the-art uncertainty quantification methods, and provides richer information for downstream decision-making tasks

Ensuring the safety of automated driving vehicles is particularly challenging due to the wide range of their operating conditions. This paper introduces CoCoSaFe, a Co mpositional Co de-level formal Sa fety verification F ram e work for automated driving controllers. Unlike traditional verification methods, such as model-based analysis, counterexample detection by guided simulation, or runtime verification through online monitoring, our approach verifies controller implementations directly at code level in an offline setting. Compositional contracts and bounded model checking are employed to assess the implementation of subsystem controllers against invariant sets. For neural network-based controllers, we introduce a scalable three-step decomposition method that utilizes a neural network verifier. CoCoSaFe is applied to adaptive cruise and lane-keeping controllers, for which we derive formal specifications and analytical models of the desired longitudinal and lateral behaviors, amenable for decoupled invariant sets. Various types of traditional and neural network controllers are verified in the order of minutes, showcasing its broad applicability and effectiveness in ensuring behavioral safety of software for automated driving and similar cyber–physical systems.

Deploying deep learning models in safety-critical applications remains a very challenging task, mandating the provision of assurances for the dependable operation of these models. Uncertainty quantification (UQ) methods estimate the model’s confidence per prediction, informing decision-making by considering the effect of randomness and model misspecification. Despite the advances of state-of-the-art UQ methods, they are computationally expensive or produce conservative prediction sets/intervals. We introduce MC-CP, a novel hybrid UQ method that combines a new adaptive Monte Carlo (MC) dropout method with conformal prediction (CP). MC-CP adaptively modulates the traditional MC dropout at runtime to save memory and computation resources, enabling predictions to be consumed by CP, yielding robust prediction sets/intervals. Throughout comprehensive experiments, we show that MC-CP delivers significant improvements over comparable UQ methods, like MC dropout, RAPS and CQR, both in classification and regression benchmarks. MC-CP can be easily added to existing models, making its deployment simple. The MC-CP code and replication package is available at https://github.com/team-daniel/MC-CP.

Abstract The formal safety analysis of automated driving vehicles poses unique challenges due to their dynamic operating conditions and significant complexity. This paper presents a case study of applying formal safety verification to adaptive cruise controllers. Unlike the majority of existing verification approaches in the automotive domain, which only analyze (potentially imperfect) controller models, employ simulation to find counter-examples or use online monitors for runtime verification, our method verifies controllers at code level by utilizing bounded model checking. Verification is performed against an invariant set derived from formal specifications and an analytical model of the required behavior. For neural network controllers, we propose a scalable three-step decomposition, which additionally uses a neural network verifier. We show that both traditionally implemented as well as neural network controllers are verified within minutes. The dual focus on formal safety and implementation verification provides a comprehensive framework applicable to similar cyber-physical systems.

Tree-based model editors and hybrid graphical-textual model editors have advantages and limitations when editing domain models. Data is displayed hierarchically in tree-based model editors, whereas hybrid graphical-textual model editors capture high-level domain concepts graphically and low-level domain details textually. We conducted an empirical user study with 22 participants to evaluate the implicit assumption of system modellers that hybrid notations are superior, and to investigate the tradeoffs between the default EMF-based tree model editor and a Sirius/Xtext-based hybrid model editor. The results of the user study indicate that users largely prefer the hybrid editor and are more confident with hybrid notations for understanding the meaning of conditions. Furthermore, we found that the tree editor provided superior performance for analysing ordered lists of model elements, whereas activities requiring the comprehension or modelling of complex conditions were carried out faster through the hybrid editor.

This paper presents the Ontology Language for the Dependability of Automated Systems (OLDAS), a modeling language based on Unified Modeling Language (UML) that aims to support dependability assessment for Automated Systems (ASs), i.e., systems intended to perform a function with minimal or no human intervention. OLDAS extends the Unified Foundational Ontology (UFO) and embeds validation rules to prevent constraint violations in ASs analysis. Specifically, the paper presents how OLDAS can support different activities during the design of ASs, from the definition of the Operational Design Domain to scenario-based analysis. OLDAS is available as a plugin of the open-source Papyrus for Robotics framework.

The performance of state-of-the-art Deep Learning models heavily depends on the availability of well-curated training and testing datasets that sufficiently capture the operational domain. Data augmentation is an effective technique in alleviating data scarcity, reducing the time-consuming and expensive data collection and labelling processes. Despite their potential, existing data augmentation techniques primarily focus on simple geometric and colour space transformations, like noise, flipping and resizing, producing datasets with limited diversity. When the augmented dataset is used for testing the Deep Learning models, the derived results are typically uninformative about the robustness of the models. We address this gap by introducing GENFUZZER, a novel coverage-guided data augmentation fuzzing technique for Deep Learning models underpinned by generative AI. We demonstrate our approach using widely-adopted datasets and models employed for image classification, illustrating its effectiveness in generating informative datasets leading up to a 26% increase in widely-used coverage criteria.

More often than not, the algorithms implemented by software systems continue to operate correctly when executed on different platforms or with different inputs, and can be easily replaced with functionally equivalent ones. However, such changes can have a significant and difficult to predict impact on the software performance, resource use, and other key quality properties. The paper introduces a method for the formal analysis of timing, resource use, cost and other quality aspects of computer programs, and a tool that automates the application of the method to Java code. A tool-supported probabilistic program performance analysis (PROPER) method was developed, and was evaluated using Java code from the Apache Commons Math library, the Android messaging app Telegram, and open-source implementations of the knapsack, binary search, and minimum path sum algorithms. PROPER synthesises a parametric Markov-chain model of the analysed code, uses information from program logs to calculate confidence intervals for the parameters of this model, and employs formal verification with confidence intervals to obtain confidence intervals for the performance properties of interest. A PROPER variant that operates with point estimates instead of confidence intervals can be used when large program logs are available. The PROPER point estimates for the analysed performance properties were accurate within 7.9% and 1.75% of the ground truth when using program logs with 103 and 104 entries, respectively. All PROPER confidence intervals for these properties contained the true property value, and became narrower when larger logs were used in the analysis. The analyses were completed in under 15 ms for point estimates, and in between 6.7 s and 7.8 s for confidence intervals on a regular laptop computer. PROPER can synthesise and reuse a parametric Markov model to accurately predict how software performance would change if the code ran on a different hardware platform, used a new function library, or had a different usage profile—supporting practitioners who are interested in these analyses.

Abstract Multi-robot systems are increasingly deployed to provide services and accomplish missions whose complexity or cost is too high for a single robot to achieve on its own. Although multi-robot systems offer increased reliability via redundancy and enable the execution of more challenging missions, engineering these systems is very complex. This complexity affects not only the architecture modelling of the robotic team but also the modelling and analysis of the collaborative intelligence enabling the team to complete its mission. Existing approaches for the development of multi-robot applications do not provide a systematic mechanism for capturing these aspects and assessing the robustness of multi-robot systems. We address this gap by introducing ATLAS, a novel model-driven approach supporting the systematic design space exploration and robustness analysis of multi-robot systems in simulation. The ATLAS domain-specific language enables modelling the architecture of the robotic team and its mission and facilitates the specification of the team’s intelligence. We evaluate ATLAS and demonstrate its effectiveness in three simulated case studies: a healthcare Turtlebot-based mission and two unmanned underwater vehicle missions developed using the Gazebo/ROS and MOOS-IvP robotic platforms, respectively.

We present an efficient parametric model checking technique for the analysis of softwareperformability, i.e., of the performance and dependability properties of software systems. The new parametric model checking (pMC) technique works by using a heuristic to automatically decompose a parametric discrete-time Markov chain (pDTMC) model of the software system under verification into fragments that can be analysed independently, yielding results that are then combined to establish the required software performability properties. Our fast parametric model checking (fPMC) technique enables the formal analysis of software systems modelled by pDTMCs that are too complex to be handled by existing pMC methods. Furthermore, for many pDTMCs that state-of-the-art parametric model checkers can analyse, fPMC produces solutions (i.e., algebraic formulae) that are simpler and much faster to evaluate. We show experimentally that adding fPMC to the existing repertoire of pMC methods improves the efficiency of parametric model checking significantly, and extends its applicability to software systems with more complex behaviour than currently possible.

Dynamic Dependability Management (DDM) is a promising approach to guarantee and monitor the ability of safety-critical Automated Systems (ASs) to deliver the intended service with an acceptable risk level. However, the non-interpretability and lack of specifications of the Learning-Enabled Components (LECs) used in ASs make this mission particularly challenging. Some existing DDM techniques overcome these limitations by using probabilistic environmental perception knowledge associated with predicting behavior changes for the agents in the environment. We propose to improve these techniques with a supervisory system that considers hazard analysis and risk assessment from the design stage. This hazard analysis is based on a characterization of the AS's operational domain (i.e., its scenario space, including unsafe ones). The proposed supervisory system also considers the uncertainty estimation and interaction between AS components through the whole perception-planning-control pipeline. Our framework then proposes leveraging and handling uncertainty from LEC components toward building safer ASs.

Abstract: As the size of software and system models grows, scalability issues in the current generation of model management languages (e.g. transformation, validation) and their supporting tooling become more prominent. To address this challenge, execution engines of model management programs need to become more efficient in their use of system resources. This paper presents an approach for partial loading of large models that reside in graph-database-backed model repositories. This approach leverages sophisticated static analysis of model management programs and auto-generation of graph (Cypher) queries to load only relevant model elements instead of naively loading the entire models into memory. Our experimental evaluation shows that our approach enables model management programs to process larger models, faster, and with a reduced memory footprint compared to the state of the art.

We introduce a tool-supported method for the formal analysis of timing, resource use, cost and other quality aspects of computer programs. The new method synthesises a Markov-chain model of the analysed code, computes this quantitative model’s transition probabilities using information from program logs, and employs probabilistic model checking to evaluate the performance properties of interest. Unlike existing solutions, our method can reuse the probabilistic model to accurately predict how the program performance would change if the code ran on a different hardware platform, used a new function library, or had a different usage profile. We show the effectiveness of our method by using it to analyse the performance of Java code from the Apache Commons Math library, the Android messaging app Telegram, and an implementation of the knapsack algorithm.

Parametric model checking (PMC) computes algebraic formulae that express key non-functional properties of a system (reliability, performance, etc.) as rational functions of the system and environment parameters. In software engineering, PMC formulae can be used during design, e.g., to analyse the sensitivity of different system architectures to parametric variability, or to find optimal system configurations. They can also be used at runtime, e.g., to check if non-functional requirements are still satisfied after environmental changes, or to select new configurations after such changes. However, current PMC techniques do not scale well to systems with complex behaviour and more than a few parameters. Our paper introduces a fast PMC (fPMC) approach that overcomes this limitation, extending the applicability of PMC to a broader class of systems than previously possible. To this end, fPMC partitions the Markov models that PMC operates with into fragments whose reachability properties are analysed independently, and obtains PMC reachability formulae by combining the results of these fragment analyses. To demonstrate the effectiveness of fPMC, we show how our fPMC tool can analyse three systems (taken from the research literature, and belonging to different application domains) with which current PMC techniques and tools struggle.

We present a new approach for synthesising Paretooptimal Markov decision process (MDP) policies that satisfy complex combinations of quality-of-service (QoS) software requirements. These policies correspond to optimal designs or configurations of software systems, and are obtained by translating MDP models of these systems into parametric Markov chains, and using multi-objective genetic algorithms to synthesise Pareto-optimal parameter values that define the required MDP policies. We use case studies from the service-based systems and robotic control software domains to show that our MDP policy synthesis approach can handle a wide range of QoS requirement combinations unsupported by current probabilistic model checkers. Moreover, for requirement combinations supported by these model checkers, our approach generates better Pareto-optimal policy sets according to established quality metrics.

Multi-robot systems are increasingly deployed to provide services and accomplish missions whose complexity or cost is too high for a single robot to achieve on its own. Although multi-robot systems offer increased reliability via redundancy and enable the execution of more challenging missions, engineering these systems is very complex. This complexity affects not only the architecture modelling of the robotic team but also the modelling and analysis of the collaborative intelligence enabling the team to complete its mission. Existing approaches for the development of multi-robot applications do not provide a systematic mechanism for capturing these aspects and assessing the robustness of multi-robot systems. We address this gap by introducing ATLAS, a novel model-driven approach supporting the systematic robustness analysis of multi-robot systems in sim-illation. The ATLAS domain-specific language enables modelling the architecture of the robotic team and its mission, and facilitates the specification of the team's intelligence. We evaluate ATLAS and demonstrate its effectiveness on two oceanic exploration missions performed by a team of unmanned underwater vehicles developed using the MOOS-IvP robotic simulator.

In this paper, software patches modifying a single line (aka 1-edit degree patches) of buggy Java open-source projects have been generated automatically using computational search and experimentally evaluated. We carried out the presumably largest to date experiment related to 1-edit degree patches, consisting of almost 27,000 computational jobs upper bounded with 107,000 computational hours. Our experiments show the benefits and drawbacks of such kind of patches. In particular, the search space size has been shown to be reduced by several orders of magnitude. The volume of tests that can be filtered out without any negative impact while generating 1-edit degree patches has been increased by about 97%. Finally, the effectiveness of finding 1-edit plausible patches is compared with multi-line plausible patches found with state-of-the-art syntax-based Automatic Program Repair tools. It is shown that despite patching fewer bugs in total, 1-edit degree patches have potential to patch some extra bugs.

Deep Learning (DL) systems are key enablers for engineering intelligent applications due to their ability to solve complex tasks such as image recognition and machine translation. Nevertheless, using DL systems in safety- and security-critical applications requires to provide testing evidence for their dependable operation. Recent research in this direction focuses on adapting testing criteria from traditional software engineering as a means of increasing confidence for their correct behaviour. However, they are inadequate in capturing the intrinsic properties exhibited by these systems. We bridge this gap by introducing DeepImportance, a systematic testing methodology accompanied by an Importance-Driven (IDC) test adequacy criterion for DL systems. Applying IDC enables to establish a layer-wise functional understanding of the importance of DL system components and use this information to assess the semantic diversity of a test set. Our empirical evaluation on several DL systems, across multiple DL datasets and with state-of-the-art adversarial generation techniques demonstrates the usefulness and effectiveness of DeepImportance and its ability to support the engineering of more robust DL systems.

Recent probabilistic model checking techniques can verify reliability and performance properties of software systems affected by parametric uncertainty. This involves modelling the system behaviour using interval Markov chains, i.e., Markov models with transition probabilities or rates specified as intervals. These intervals can be updated continually using Bayesian estimators with imprecise priors, enabling the verification of the system properties of interest at runtime. However, Bayesian estimators are slow to react to sudden changes in the actual value of the estimated parameters, yielding inaccurate intervals and leading to poor verification results after such changes. To address this limitation, we introduce an efficient interval change-point detection method, and we integrate it with a state-of-the-art Bayesian estimator with imprecise priors. Our experimental results show that the resulting end-to-end Bayesian approach to change-point detection and estimation of interval Markov chain parameters handles effectively a wide range of sudden changes in parameter values, and supports runtime probabilistic model checking under parametric uncertainty.

The wide use of robotic systems contributed to developing robotic software highly coupled to the hardware platform running the robotic system. Due to increased maintenance cost or changing business priorities, the robotic hardware is infrequently upgraded, thus increasing the risk for technology stagnation. Reducing this risk entails migrating the system and its software to a new hardware platform. Conventional software engineering practices such as complete re-development and code-based migration, albeit useful in mitigating these obsolescence issues, they are time-consuming and overly expensive. Our RoboSMi model-driven approach supports the migration of the software controlling a robotic system between hardware platforms. First, RoboSMi executes static analysis on the robotic software of the source hardware platform to identify platform-dependent and platform-agnostic software constructs. By analysing a model that expresses the architecture of robotic components on the target platform, RoboSMi establishes the hardware configuration of those components and suggests software libraries for each component whose execution will enable the robotic software to control the components. Finally, RoboSMi through code-generation produces software for the target platform and indicates areas that require manual intervention by robotic engineers to complete the migration. We evaluate the applicability of RoboSMi and analyse the level of automation and performance provided from its use by migrating two robotic systems deployed for an environmental monitoring and a line following mission from a Propeller Activity Board to an Arduino Uno.

Abstract UML profiles offer an intuitive way for developers to build domain-specific modelling languages by reusing and extending UML concepts. Eclipse Papyrus is a powerful open-source UML modelling tool which supports UML profiling. However, with power comes complexity, implementing non-trivial UML profiles and their supporting editors in Papyrus typically requires the developers to handcraft and maintain a number of interconnected models through a loosely guided, labour-intensive and error-prone process. We demonstrate how metamodel annotations and model transformation techniques can help manage the complexity of Papyrus in the creation of UML profiles and their supporting editors. We presentJorvik, an open-source tool that implements the proposed approach. We illustrate its functionality with examples, and we evaluate our approach by comparing it against manual UML profile specification and editor implementation using a non-trivial enterprise modelling language (Archimate) as a case study. We also perform a user study in which developers are asked to produce identical editors using both Papyrus andJorvikdemonstrating the substantial productivity and maintainability benefits thatJorvikdelivers.

Deep Neural Networks (DNNs) are increasingly deployed in safety-critical applications including autonomous vehicles and medical diagnostics. To reduce the residual risk for unexpected DNN behaviour and provide evidence for their trustworthy operation, DNNs should be thoroughly tested. The DeepFault whitebox DNN testing approach presented in our paper addresses this challenge by employing suspiciousness measures inspired by fault localization to establish the hit spectrum of neurons and identify suspicious neurons whose weights have not been calibrated correctly and thus are considered responsible for inadequate DNN performance. DeepFault also uses a suspiciousness-guided algorithm to synthesize new inputs, from correctly classified inputs, that increase the activation values of suspicious neurons. Our empirical evaluation on several DNN instances trained on MNIST and CIFAR-10 datasets shows that DeepFault is effective in identifying suspicious neurons. Also, the inputs synthesized by DeepFault closely resemble the original inputs, exercise the identified suspicious neurons and are highly adversarial.

Software systems are increasingly expected to cope with variable workloads, component failures and other uncertainties through self-adaptation. As such, self-adaptive software has been the subject of intense research over the past decade [3, 4, 9, 10].

An increasingly used method for the engineering of software systems with strict quality-of-service (QoS) requirements involves the synthesis and verification of probabilistic models for many alternative architectures and instantiations of system parameters. Using manual trial-and-error or simple heuristics for this task often produces suboptimal models, while the exhaustive synthesis of all possible models is typically intractable. The EvoChecker search-based software engineering approach presented in our paper addresses these limitations by employing evolutionary algorithms to automate the model synthesis process and to significantly improve its outcome. EvoChecker can be used to synthesise the Pareto-optimal set of probabilistic models associated with the QoS requirements of a system under design, and to support the selection of a suitable system architecture and configuration. EvoChecker can also be used at runtime, to drive the efficient reconfiguration of a self-adaptive software system. We evaluate EvoChecker on several variants of three systems from different application domains, and show its effectiveness and applicability.

We describe a tool-supported method for the efficient synthesis of parametric continuous-time Markov chains (pCTMC) that correspond to robust designs of a system under development. The pCTMCs generated by our RObust DEsign Synthesis (RODES) method are resilient to changes in the system’s operational profile, satisfy strict reliability, performance and other quality constraints, and are Pareto-optimal or nearly Pareto-optimal with respect to a set of quality optimisation criteria. By integrating sensitivity analysis at designer-specified tolerance levels and Pareto optimality, RODES produces designs that are potentially slightly suboptimal in return for less sensitivity—an acceptable trade-off in engineering practice. We demonstrate the effectiveness of our method and the efficiency of its GPU-accelerated tool support across multiple application domains by using RODES to design a producer-consumer system, a replicated file system and a workstation cluster system.

Building on concepts drawn from control theory, self-adaptive software handles environmental and internal uncertainties by dynamically adjusting its architecture and parameters in response to events such as workload changes and component failures. Self-adaptive software is increasingly expected to meet strict functional and non-functional requirements in applications from areas as diverse as manufacturing, healthcare and finance. To address this need, we introduce a methodology for the systematic ENgineering of TRUstworthy Self-adaptive sofTware (ENTRUST). ENTRUST uses a combination of (1) design-time and runtime modelling and verification, and (2) industry-adopted assurance processes to develop trustworthy self-adaptive software and assurance cases arguing the suitability of the software for its intended application. To evaluate the effectiveness of our methodology, we present a tool-supported instance of ENTRUST and its use to develop proof-of-concept self-adaptive software for embedded and service-based systems from the oceanic monitoring and e-finance domains, respectively. The experimental results show that ENTRUST can be used to engineer self-adaptive software systems in different application domains and to generate dynamic assurance cases for these systems.

We present a method for the synthesis of software system designs that satisfy strict quality requirements, are Pareto-optimal with respect to a set of quality optimisation criteria, and are robust to variations in the system parameters. To this end, we model the design space of the system under development as a parametric continuous-time Markov chain (pCTMC) with discrete and continuous parameters that correspond to alternative system architectures and to the ranges of possible values for configuration parameters, respectively. Given this pCTMC and required tolerance levels for the configuration parameters, our method produces a sensitivity-aware Pareto-optimal set of designs, which allows the modeller to inspect the ranges of quality attributes induced by these tolerances, thus enabling the effective selection of robust designs. Through application to two systems from different domains, we demonstrate the ability of our method to synthesise robust designs with a wide spectrum of useful tradeoffs between quality attributes and sensitivity.

The formal verification of finite-state probabilistic models supports the engineering of software with strict quality-of-service (QoS) requirements. However, its use in software design is currently a tedious process of manual multiobjective optimisation. Software designers must build and verify probabilistic models for numerous alternative architectures and instantiations of the system parameters. When successful, they end up with feasible but often suboptimal models. The EvoChecker search-based software engineering approach and tool introduced in our paper employ multiobjective optimisation genetic algorithms to automate this process and considerably improve its outcome. We evaluate EvoChecker for six variants of two software systems from the domains of dynamic power management and foreign exchange trading. These systems are characterised by different types of design parameters and QoS requirements, and their design spaces comprise between 2E+14 and 7.22E+86 relevant alternative designs. Our results provide strong evidence that EvoChecker significantly outperforms the current practice and yields actionable insights for software designers.

Software project managers are often faced with challenges when trying to effectively staff and schedule projects. Incorrectly planning and estimating the execution of tasks frequently causes software projects to be delivered late and/or over budget, whereas not selecting the appropriate developers to carry out tasks may produce lower-quality, defective software products. To combat these challenges, this paper presents IntelliSPM -- a tool aiming to support software project management activities consisting of several optimization mechanisms borrowed from the area of Computational Intelligence. The tool takes into account technical aspects but also significant human factors, which have been found to play a crucial role in software quality and developer productivity. The purpose of IntelliSPM is to offer suggestions to project managers containing a set of possible project schedules and staffing strategies that minimizes duration and maximizes resource usage. Several simulated and real-world projects were used during the validation process, with results showing that IntelliSPM is capable of providing that much-needed practical benefit to software companies to improve various aspects of development, such as performance and job satisfaction, whilst keeping within the general objectives and particular constraints of each software project.