Researchers from the ADVANCE project will organize a graduate school on the Verification and Validation (V&V) of Future Cyber-Physical Systems. The school will provide an

• overview of typical V&V challenges of large-scale safety-critical systems, illustrated by the space and automotive domain,
• new design, verification and analysis techniques for CPS, e.g. using machine learning or model-based techniques,
• a discussion panel on using AI techniques in verification and verifying AI-based systems.

Target audience: the lectures are aimed at MSc or early PhD students, who have a basic understanding of software/systems engineering concepts.

Format: the school will be fully online to encourage participation of students. The timing of the school is accessible both from Europe and South America.

Registration: the school will be FREE (supported by the ADVANCE EU project), but registration will be required: https://forms.office.com/e/p0NxXhedCw 

Tentative program

Lectures and presenters

The ADVANCE project

• Abstract: In the last decade, technology has rapidly expanded to multiple aspects of our lives. The physical world is being constantly enhanced by technology and connectivity, for reasons ranging from improvement in our lives to pure entertainment. Examples of this trend are evident in emerging technologies like autonomous transportation, smart cities, home and industry automation. The scientific community identifies such kind of systems as Cyber-Physical Systems (CPSs), that is, systems where the physical aspects are deeply integrated with the communication and computing (cyber) parts.
  
  The tight interaction with the physical world often means that CPSs, if not operating properly, can cause harm to users and/or the environment. In other words, CPSs are often safety-critical systems, and must therefore be subject to a rigorous Verification and Validation (V&V) process to heck if they meet the specifications and fulfill the intended use, goals and objectives. This talk provides an overview on the ADVANCE project, whose scientific objective is to conceive new approaches to support the Verification and Validation (V&V) of Cyber-Physical Systems (CPS). In order to achieve this goal, the project consortium is researching new techniques, methods, and tools to improve the effectiveness and efficacy of the V&V process. Furthermore, the ADVANCE project also has the strategic objective of creating an international network of expertise and collaboration in the context of V&V of cyber-physical systems, and training skilled professionals in V&V, software testing, and Information and Communication Technology (ICT).
• Speaker: Paolo Lollini (UNIFI)

Dealing with Zero-Day Attacks through Unsupervised Anomaly-Based Intrusion Detection

• Abstract: Anomaly detection aims at identifying patterns in data that do not conform to the expected behaviour, relying on machine-learning algorithms that are suited for binary classification. It has been arising as one of the most promising techniques to suspect attacks or failures, as it has the potential to identify errors due to unknown faults as well as intrusions and zero-day attacks. This tutorial will discuss in detail attack detection through unsupervised anomaly detection, and will review the construction of an evaluation campaign through i) the identification of the attack models and datasets, ii) the selection and discussion of unsupervised algorithms, iii) the identification of target metrics, iv) the execution of the algorithms and v) their comparison. Attendees will also be involved in an hands-on session where algorithms will be executed on public attack datasets thanks to Python scripts, which will be provided to the audience and are ready to be executed also by non-experts that start approaching binary classification using ML algorithms.
• Speakers: Tommaso Zoppi, Andrea Bondavalli (CINI UNIFI)

The ISO26262:2018 Functional Safety Standard for Road Vehicles

• Abstract: This talk provides a high level introduction to the Functional Safety Standards commonly used to achieve functional safety in modern safety critical product and infrastructures. In particular the ISO26262:2018 safety standards for Functional safety in Road Vehicles will be presented and explained. It will be provided a close view of the project independent processes that shall be well established in companies operating in such domains as well as project dependent activities that aims to reduce the occurrence of systematic and random failures in automotive systems in order to be compliant to the four Automotive Safety Integrity Levels (ASIL A B C D).
• Speakers: Francesco Brancati (ResilTech)

Verification and Validation in the context of space system engineering

• Abstract: System engineering is the disciplined understanding of “how all the pieces work together”. Space system engineering approaches are applicable at all levels of the space sector by individuals with such varied positions as spacecraft system engineer, mission designer, and Minister of Space. The lecture introduces the key elements of a space mission and focuses on the role of the requirements specification, verification and validation for achieving a desirable end product. Using the BEDCS case study offered by INPE for the ADVANCE project, the life cycle of a space mission will be highlighted. The objective is to discuss how a balanced solution for a space system can be verified and validated to meet the expectations of the “stakeholders” throughout the entire life cycle of the system.   
• Speaker: Fátima Mattiello (INPE)

Qualitative modeling: foundations and applications

• Abstract: A critical factor in the quality of any model-based design and V&V is the faithfulness of the underlying model. The domain expert who creates and verifies the models and interprets and explains the results of the V&V process plays a key role here. Human, particularly technical thinking, is qualitative (small-medium-large, slow-fast). Qualitative modeling and reasoning automate this thinking with a sound mathematical basis and efficient IT implementation. Its basic idea is to cluster domains of continuous values exposing identical phenomena into a single qualitative value. This discrete abstraction results in high information compression, simultaneously preserving the essential properties. It facilitates the use of a vast repertoire of discrete formal methods. The qualitative models and analysis results are well-explainable thanks to being close to engineering thinking.
• Speaker: András Pataricza (BME)

Impact Analysis in IT/OT Systems

• Abstract: The increased cyber-attack surface in Cyber-Physical Systems, the close coupling to vulnerable physical processes, and the potential for human casualties necessitate a careful extension of traditional safety methodologies, e.g., error propagation analysis (EPA),  with cybersecurity capabilities. Successful attacks intruding on the physical part of the system can cause severe or even catastrophic losses. The talk focuses on a model-based system engineering (MBSE) solution for the assessment and mitigation strategy design approach where the proper quality of the security assessment is assured by using embedded formal methods.
• Speaker: András Földvári (BME)

Model-Based Systems Engineering: When, How and Why to Use It?

• Abstract: Model-based systems engineering (MBSE) is gaining prevalence in the development of complex cyber-physical systems, among others, in nanosatellites used in different space missions. MBSE approaches promote the application of reusable models defined in high-level modeling languages, e.g., SysML. Such languages provide means to define the system in a platform-independent way, both in terms of component behavior and system structure. The emergent models then can be tailored to various platforms to support the conduction of various functional and extra-functional analyses and the automated generation of implementation or configuration artifacts utilizing integrated tool support. This lecture overviews the foundations of MBSE, including its basic concepts, different aspects of modeling and prevalent modeling methodologies. Next, it introduces concepts related to platform-based design and outlines some general principles that should be followed in the process. Finally, the lecture overviews different types of modeling languages and tools that can be used for the design and analysis of the system in different development stages. The lecture relies on the Gamma Statechart Composition Framework, an open source modeling tool for the component-based design and analysis of reactive systems, to showcase the power of tool-supported MBSE while incorporating examples from the aerospace industry.
• Speaker: Bence Graics (BME)

Safe Reinforcement Learning

• Abstract: This talk delves into the critical intersection of reinforcement learning (RL) and safety, highlighting how this dynamic field holds the key to developing intelligent systems that can operate reliably in complex and uncertain environments. As industries continue to integrate AI and automation, ensuring the safety of these systems becomes paramount. The presentation will introduce the foundational concepts of RL and its applications, emphasizing how RL algorithms can learn from both successes and failures to make informed decisions while adhering to safety constraints. Through a selection of case studies from autonomous vehicles, industrial automation, and healthcare, the audience will gain insights into how RL can be tailored to address safety concerns. Moreover, the talk will explore cutting-edge techniques that integrate safety considerations directly into the RL framework, enabling the creation of systems that not only learn optimally but also prioritize safety at all times. 
• Speaker: Esther Colombini (Unicamp)

Fault Injection Techniques: overview of recent advances

• Abstract: Software-implemented fault injection uses software-based approaches to emulate the effect of faults in a real system. It produces representative results that are accurate and similar to those caused by 'true' faults, while taking advantage of the flexibility and controllability of software-based methods. These characteristics have made it a perfect technique for ensuring safety and evaluating the dependability of any type of system, including those that are sent to outer space. In this module, we will look into the most common approaches for emulating hardware and software faults and briefly discuss possible optimizations, providing an overview of the recent advances in fault injection in different application domains.
• Speaker: Frederico Cerveira (CISUC)

Robustness testing of REST services

• Abstract: REST services are nowadays being used to support many businesses, with most major companies exposing their services via REST interfaces (e.g., Google, Amazon, Instagram, and Slack). In this type of scenarios, heterogeneity is prevalent and software is sometimes exposed to unexpected conditions that may activate residual bugs, leading service operations to fail. Such failures may lead to financial or reputation losses (e.g., information disclosure). Although techniques and tools for assessing robustness have been thoroughly studied and applied to a large diversity of domains, REST services still lack practical approaches that specialize in robustness evaluation. In this presentation, we introduce a tool (named bBOXRT) for performing robustness tests over REST services, solely based on minimal information expressed in their interface descriptions. We used bBOXRT to evaluate an heterogeneous set of 52 REST services that comprise 1,351 operations and fit in distinct categories (e.g., public, private, in-house). We were able to disclose several different types of robustness problems, including issues in services with strong reliability requirements and also a few security vulnerabilities. The results show that REST services are being deployed preserving software defects that harm service integration, and also carrying security vulnerabilities that can be exploited by malicious users.
• Speaker: Nuno Laranjeiro (CISUC)

Using Fault Injection in CubeSat System

• Abstract: CubeSats are an established trend in the space industry.  The CubeSat standard opens opportunities for rapid and low-cost access to space. The use of COTS components instead of space-hardened hardware greatly reduces the cost of CubeSat-based missions and provides the additional benefit of increasing software functionalities at a low power consumption. However, COTS components are not designed for the space environment, making CubeSats sensitive to space radiation. This means that CubeSats need additional software mechanisms to guarantee resilient behavior in the presence of space radiation. Our idea is that such software implemented fault tolerance mechanisms must be tailored to the specific code running in each CubeSat and the logical way to achieve that is to extend the software development process for CubeSats to include the systematic resilience evaluation of software as part of the CubeSats software lifecycle process.
  
  This presentation proposes a set of structured steps to enhance the classic software development process used in CubeSats, focusing particularly on the Verification and Validation (V&V) phase. The approach uses fault injection as an integral part of the development environment for CubeSats software and includes three major steps: a) sensitivity evaluation (verification) of software in the presence of faults caused by space radiation, b) strengthen of the software with targeted software implemented fault tolerance (SWIFT) mechanisms and c) validation of the effectiveness of the SWIFT mechanisms to confirm that the software is immune to space radiation faults. These added steps to the V&V process must be carried out during software development, as well as every time the CubeSat software has an update, or even a minor change, to ensure that the impact of faults caused by space radiation is tolerated by the CubeSat software.
  
  The talk will present the necessary background on fault injection and on software implemented fault tolerance and presents three examples of embedded software running in the EDC (Environment Data Collection) CubeSat board, which is part (payload) of a constellation of satellites being developed by the Brazilian National Institute for Space Research (INPE). EDC use case  provides a realistic insight on the effectiveness of the proposed steps. Our results show that the proposed approach can reduce the percentage of silent data corruption (the most problematic failure mode) from the range of 15% to less than 1% and even to 0% in some embedded software, meaning that the CubeSat software becomes immune to space radiation.

• Speaker: Henrique Madeira (UC)

Stochastic modeling and optimization in CPS

• Abstract: Cyber-Physical-Systems (CPS) are exposed to changing exogenous conditions, such as the demand for services, alterations in the physical world or its virtual representation, and natural or targeted hazards, among others. Modeling the stochastic context of CPS is crucial, not just in terms of characterizing or anticipating behaviors, but also to evaluate whether the existing decision rules satisfy objectives related to resilience and risk (including V&V), and to what extent these may be improved. The proliferation of digital technologies (e.g., IoT, machine learning) allows data-driven analysis of systems such as energy grids, supply chains, or smart factories. This talk focuses on the potential of stochastic optimization to enhance decision-making in such systems by means of the articulation of data analytics, simulation, and optimization techniques. Specifically, the session demonstrates the use of exact and approximate optimization techniques in conjunction with probabilistic modeling to address decision problems in CPS.
• Speaker: Camilo Gómez (Uniandes)