Sinem Getir Yaman

The increasing deployment of Unmanned Surface Vessels (USVs) and Maritime Autonomous Surface Ships (MASS) requires tighter integration of safety and cyber-security analysis. Current approaches often treat these concerns separately, overlooking the causal pathways through which cyberattacks can degrade safety-critical functions. This paper addresses this gap using the Structural Causal World Model (SCWM), a layered causal modelling framework with explicit uncertainty semantics and safety-metric bindings. SCWM represents system attributes as nodes in a semantically typed directed acyclic causal structure and enables the extraction of attack-induced propagation subgraphs linking cyber-security violations to collision risk indicators. We present the MASS-SCWM framework and demonstrate its application to compound attacks targeting vessel communications and vision-based perception systems, including loss of connectivity with the Remote Operations Centre and misclassification or range estimation errors in object detection. These attacks are modelled as attribute-level perturbations whose effects propagate through belief dynamics and decision layers to safety metrics such as Closest Point of Approach (CPA) and Time to CPA (TCPA). The framework enables structured and quantitatively comparable analysis of compound attack scenarios and protection mechanisms. By formally binding cyber-security assumptions to safety guarantees within a unified causal structure, MASS-SCWM provides a principled foundation for integrated safety–security assurance aligned with emerging regulatory expectations for MASS systems.

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.

Autonomous agents are increasingly deployed in sensitive, human-centric domains—such as healthcare, assistive care, and emergency response—where their decision-making must align with complex human norms. These translate into Social, Legal, Ethical, Empathetic, and Cultural (SLEEC) requirements that are often nuanced and context-dependent, challenging traditional software engineering paradigms. Our tutorial paper presents a comprehensive, tool-supported methodology for managing the SLEEC requirements lifecycle, covering elicitation, well-formedness validation, and conformance verification of software design models against SLEEC requirements. We demonstrate the use of our methodology and associated tools through application to a robot-assisted dressing system, providing a guide for researchers and engineers to bridge the gap between abstract human norms and verifiable system designs.

Recent advances in generative AI and machine learning have stirred up fears about the unbridled adoption of autonomous, self-adaptive decision mechanisms in socio-technical systems. This vision paper explores the critical relationship between software-intensive systems and the empowerment of humans as individuals and society. We highlight the need for human empowerment within the context of self-adaptive socio-technical systems (SASTSs), which require mechanisms for balancing of diverse needs, values, and ethics on the individual, community, and societal levels. We propose an architecture comprised of Connector and Mediator elements, and third-party auditing, to support interactions and ensure preservation of human needs, values, and ethics. We use an example of Robot-Assisted A&E Triage system to motivate and illustrate our work and discuss some open challenges for future research.

As software systems increasingly interact with humans in application domains such as transportation and healthcare, they raise concerns related to the social, legal, ethical, empathetic, and cultural (SLEEC) norms and values of their stakeholders. Normative non-functional requirements (N-NFRs) are used to capture these concerns by setting SLEEC-relevant boundaries for system behavior. Since N-NFRs need to be specified by multiple stakeholders with widely different, non-technical expertise (ethicists, lawyers, regulators, end users, etc.), N-NFR elicitation is very challenging. To address this difficult task, we introduce N-Check, a novel tool-supported formal approach to N-NFR analysis and debugging. N-Check employs satisfiability checking to identify a broad spectrum of N-NFR well-formedness issues, such as conflicts, redundancy, restrictiveness, and insufficiency, yielding diagnostics that pinpoint their causes in a user-friendly way that enables non-technical stakeholders to understand and fix them. We show the effectiveness and usability of our approach through nine case studies in which teams of ethicists, lawyers, philosophers, psychologists, safety analysts, and engineers used N-Check to analyse and debug 233 N-NFRs, comprising 62 issues for the software underpinning the operation of systems, such as, assistive-care robots and tree-disease detection drones to manufacturing collaborative robots.

Autonomous systems are often used in applications where environmental and internal changes may lead to requirement violations. Adapting to these changes proactively, i.e., before the violations occur, is preferable to recovering from the failures that may be caused by such violations. However, proactive adaptation needs methods for predicting requirement violations timely, accurately, and with acceptable overheads. To address this need, we present a method that allows autonomous systems to predict violations of performance, dependability and other nonfunctional requirements, and therefore take preventative measures to avoid or otherwise mitigate them. Our method for pre dicting these autonomou s sys t em disrupti o ns (PRESTO) comprises a design time stage and a run-time stage. At design-time, we use parametric model checking to obtain algebraic expressions that formalise the relationships between the nonfunctional properties of the requirements of interest (e.g., reliability, response time, and energy use) and the parameters of the system and its environment. At run-time, we predict future changes in these parameters by applying piece-wise linear regression to online data obtained through monitoring, and we use the algebraic expressions to predict the impact of these changes on the system requirements. We demonstrate the application of PRESTO through simulation in case studies from two different domains.