Hours:
20 hours (5 credits)

Room:

Aula Riunioni del Dipartimento di Ingegneria dell’Informazione, Via G. Caruso 16, Pisa - Ground Floor

To register to the course, click here

Short Abstract:

Safety-critical systems, including those with a high degree of autonomy, provide user interfaces that allow human operators to control and monitor the system. Software modules typically define the functionalities of the user interface, including control safety functions. To gain confidence that the system can fulfil its expected mission goals, it is therefore important that user interface software is designed to make the system easy to use and at the same time capable of correcting foreseeable mistakes that can be committed by the operator.Safety-critical systems, including those with a high degree of autonomy, provide user interfaces that allow human operators to control and monitor the system. Software modules typically define the functionalities of the user interface, including control safety functions. To gain confidence that the system can fulfil its expected mission goals, it is therefore important that user interface software is designed to make the system easy to use and at the same time capable of correcting foreseeable mistakes that can be committed by the operator.This 20-hour course will provide PhD students with knowledge and skills on advanced methods and tools for rigorous verification and validation of user interface software in safety-critical systems. Examples from the avionics and medical domain will be used through the course to ground the discussion on concrete cases and actual systems.The learning outcomes are: (i) understanding of the design challenges with user interface software in safety-critical systems; (ii) understanding of analysis methods and use-related safety requirements; (iii) understanding of verification and validation techniques based on formal (mathematical) methods; (iv) practical experience with toolkits routinely used at NASA Langley for the verification and validation of safety-critical systems, including the PVS theorem prover [3], the VSCode-PVS integrated development environment [4,5], and the DAA-Displays toolkit [6].While the focus of this course is on safety-critical systems, the presented techniques are in fact generally applicable to any software-intensive interactive system, to catch latent design anomalies early in the development process, before important design decisions are made that could be expensive to correct at later stages of the development process. 

Course Contents in brief:

1. Design challenges in user Interface software in safety-critical systems
2. Design challenges in user Interface software in safety-critical systems
3. Hazard analysis methods for software intensive safety-critical systems
4. Formal methods technologies for V&V of user interface software
5. Practical modeling and analysis experience with methods and tools routinely used at NASA Langley for the verification and validation of safety-critical systems 

Schedule:

1. 22/07/2024: 9:00-13:00
2. 23/07/2024: 9:00-13:00
3. 24/07/2024: 9:00-13:00
4. 25/07/2024: 9:00-13:00
5. 26/07/2024: 9:00-13:00