VALU3S is organizing a summer school!
The VALU3S project is proud to organize a summer school with the focus on the results produced during the project. The theme of the school is Verification and Validation of Dependable Cyber-Physical Systems, and the tentative schedule of the summer school is as follows:
| Tuesday - 18th | Wednesday - 19th | Thursday - 20th | |
|---|---|---|---|
| 9h00-10h30 |
Introduction to verification and validation of dependable cyber-physical systems
Introduction to verification and validation of dependable cyber-physical systems
Manufacturers of cyber-physical systems have been allocating an enormous amount of time and effort in the past years developing and conducting research on these systems. The effort spent has resulted in the availability of prototypes demonstrating new capabilities as well as the introduction of such systems to the market within different domains. Moreover, manufacturers of these systems have been ensuring that these systems function in the intended way and according to specifications which is not a trivial task as system complexity rises dramatically the more integrated and interconnected these systems become with the addition of automated functionality and features to them. With rising complexity, unknown emerging properties of the system may come to the surface making it necessary to conduct thorough verification and validation (V&V) of these systems. Through the V&V of these systems, the manufacturers of the systems are able to ensure safe, secure and reliable systems for society to use since failures in highly automated systems can be catastrophic. In this lecture, we present some of the most important elements of V&V activities, including the V&V methods used. We also provide an overview of the VALU3S project and present some of the results obtained in the project. This session also aims to introduce the other sessions of the summer school. |
VVML: Specifying Workflows for V&V Methods
VVML: Specifying Workflows for V&V Methods
The Verification and Validation Modelling Language (VVML) is a subset of UML’s activity diagrams, fine-tuned to describe workflows on how to use specific formal methods and tools. It includes concepts such as activities, artifacts, and composition. This language was used in the VALU3S project, where partners produced 44 workflows describing around 40 V&V methods and tools. In this session, we will (1) explain how to specify workflows in VVML, (2) illustrate some of its usages, and (3) demonstrate how to use tools to produce and to analyse VVML workflows, focusing on our plug-in for the Enterprise Architect toolset. |
Symbolic Model Checking of Hybrid Systems
Symbolic Model Checking of Hybrid Systems
The formal verification of complex control systems is often based on hybrid system models, which provide a framework that combine continuous-time dynamics of the plant with instantaneous changes in the control logic. This is fact divided into different modes, each of which is associated with a continuous dynamical system described by differential constraints. The switches between modes are instead governed by discrete events and conditions. In these settings, the specification and verification of formal temporal properties, especially in case of liveness (e.g., related stability) is quite challenging both in terms of representation and scalability. In this lecture, we will first give an overview of different approaches based on model checking and temporal logic, deductive methods, abstraction refinement, Lyapunov analysis, and simulation. We will then examine more in depth SMT-based symbolic model checking techniques. SMT gives a suitable framework for formalizing and proving temporal properties, because it combines discrete-time reasoning with background theories that can represent the continuous dynamics. The hybrid system is typically encoded as a set of logical formulas. The logical formulas represent the system dynamics, constraints, and properties to be verified. We will finally show combinations of SMT-based model checking with other techniques such as abstraction refinement, deduction of differential invariants, Lyapunov functions, and monitoring. |
| 10h30-11h00 | Break | Break | Break |
| 11h00-12h30 |
An overview to testing of safety-critical cyber-physical systems
An overview to testing of safety-critical cyber-physical systems
This summer school session provides a comprehensive overview of testing safety-critical cyber-physical systems, encompassing standards, testing techniques at different stages of the development lifecycle, fault injection, and virtual validation at system design time. Participants gain valuable insights into ensuring the dependability and safety of complex technical software-intensive systems. |
Formal requirements engineering
Formal requirements engineering
Eliciting requirements that are detailed and logical enough to be amenable to formal verification is a difficult task. Multiple tools exist for requirements elicitation and some of these also support formalisation of requirements in a way that is useful for formal methods. We report on our experience of using the Formal Requirements Elicitation Tool (FRET) to formalise requirements for an aircraft engine controller. In this context, we evaluate the use of FRET to bridge the communication gap between formal methods experts and aerospace industry specialists. We describe our journey from ambiguous, natural-language requirements to concise, formalised FRET requirements, focusing on the aircraft engine controller use case. We include our analysis of the formalised requirements from the perspective of patterns, translation into linear temporal logic (LTL) formulae and the relationship between parent-child requirements in this set. We discuss refactoring requirements to improve their readability and maintainability and demonstrate our tool support for these refactoring's in Mu-FRET. Through examples from the use case, we provide insight into lessons learned throughout this process. We also discuss toolchains available for verifying requirements formalised in this way. |
Deductive Verification in a Nutshell
Deductive Verification in a Nutshell
Deductive software verification expresses the correctness of the source code as a set of mathematical statements, called verification conditions. A human user typically contributes in two ways: formalising an informally stated specification for the source code, and providing (if necessary) guidance to a verification system to show formally the conformance of the source code to the specification. Properties to be verified are typically expressed in specification languages that combine first-order-logic and some theories (arithmetic, sets, arrays, bit vectors) to allow modelling the programming language while still allowing proof automation. These properties are verified in a modular way (e.g. method contracts using the Design by Contract paradigm, loop invariants, class invariants, lemmas, assumptions, assertions) and include both behavioural properties, e.g., calculates the longest repeated substring, and safety properties, e.g., null de-reference, out-of-bounds errors, termination, arithmetic overflow. In this session we will start by providing an introduction to deductive verification, focusing on using the Dafny language and verifier, followed by an introduction to the Coq proof assistant. More concretely, we will exploit a highly-expressive and powerful type system to specify, implement, and develop correctness proofs of functional programs. We will also extract from these proofs code that is correct-by-construction and that can be used as a safe code base for larger software implementations. |
| 12h30-14h00 | Lunch & Poster Presentation | Lunch & Poster Presentation | Lunch & Poster Presentation |
| 14h00-15h30 |
Software-implemented fault injection
Software-implemented fault injection
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. |
Introduction to Model Checking
Introduction to Model Checking
Model-checking a system involves (1) representing formally a model of the system, abstracting away many unnecessary details, (2) represent formally the requirements that must be satisfied, and finally (3) automatically verify if the model satisfies the requirements. Many formalisms exist to represent these models and these requirements, and many tools exist to verify satisfiability, known as model-checkers. In this lecture we will focus on the Spin model checker and explore how to build a formal model as a composition of smaller interacting components for Spin. We will use some of the requirements seen in the previous lecture to illustrate how to formalise them and verify them in Spin. One of the main verification challenges is to address the state-space explosion problem, for which there are relevant reductions and abstractions that will be analysed. We will describe how to extend our model and requirements with the notion of time, using the Uppaal model checker to illustrate these ideas. Richer notions of time, required by many requirements presented in the first lecture, will need a more complex notion of time. This will be covered by the following lecture. |
An overview of relevant safety and cybersecurity standards
An overview of relevant safety and cybersecurity standards
The standardization class gives an overview of the landscape of cyber physical systems, covering functional safety and cybersecurity. It will touch upon relevant standards in different domains and focus on railway (EN 50128, EN 50129), industrial control systems (IEC 61508, IEC 61511, IEC 62443), and automotive (ISO 26262, ISO/SAE 21434). |
| 15h30-16h00 | Break | Break | Break |
| 16h00-17h30 |
Simulation-based fault injection
Simulation-based fault injection
In the past few years, a paradigm called “shift-to-left” has been inspiring researchers to go towards simulation-based verification and validation of automated systems. The paradigm is being discussed to a great extent within the relevant industrial domains/communities. This has resulted in the build-up of fault injection engines as well as evaluating the safety requirements at the simulation-level. Conducting tests at the simulation level also facilitates evaluation of systems in a safe environment, something that might be costly if done when the vehicle, drone, or any other safety-critical systems are in use. Simulation-based testing, however, also comes with the drawback that the usefulness of the results obtained is tightly connected to the representativeness of the simulation environment as well as the automated features that are being evaluated. One way to close this gap is by supporting simulation-based test results with tests conducted in close-track environments or even those conducted in the field. In this session of the summer school, we present simulation-based fault injection as well as the most common approaches used to conduct this kind of testing. |
A V&V framework for storing elements of V&V activities
A V&V framework for storing elements of V&V activities
In this session, we present a multi-domain and multi-dimensional framework to characterize and classify V&V methods and tools in a structured way. The framework considers a comprehensive characterization of different relevant aspects of V&V. A web-based repository has been implemented on the basis of the framework in order to collect information about the application of V&V methods and tools. This way, practitioners and researchers can learn about and identify suitable V&V processes. In this session, in addition to explaining the framework, access to the web repository will also be provided to the students. In order to get to know the web repository, a series of exercises will be presented where students will be asked to identify the most appropriate tools and methods for different V&V needs and scenarios. |
An overview of relevant safety and cybersecurity standards
An overview of relevant safety and cybersecurity standards
The standardization class gives an overview of the landscape of cyber physical systems, covering functional safety and cybersecurity. It will touch upon relevant standards in different domains and focus on railway (EN 50128, EN 50129), industrial control systems (IEC 61508, IEC 61511, IEC 62443), and automotive (ISO 26262, ISO/SAE 21434). |
The summer school is planned to take place in Genova, Italy on 18th-20th July 2023 with the support of the partners within the Italian cluster. The estimated cost for registration (per participant) is around 180€.
If you are a student (bachelor, master, or Ph.D.) or an early-stage researcher/engineer with an interest in expanding your knowledge around verification and validation, we recommend you to join us!
Preliminary list of lecturers at the summer school:
- Joseba Agirre, Mondragon University
- Raul Barbosa, University of Coimbra
- Thomas Bauer, Fraunhofer IESE
- Sina Borrami, Alstom
- Frederico Cerveira, University of Coimbra
- Bohumil Hruška, Lieberlieber Software
- Pierre Kleberger, RISE Research Institutes of Sweden
- Jonas Melchert, Alstom
- Rosemary Monahan, Maynooth University
- David Pereira, Instituto Superior de Engenharia do Porto (ISEP)
- José Proença, Instituto Superior de Engenharia do Porto (ISEP)
- Behrooz Sangchoolie, RISE Research Institutes of Sweden
- Christoph Schmittner, AIT Austrian Institute of Technology
- Stefano Tonetta, Fondazione Bruno Kessler (FBK)