Semantic Techniques for Verification and Validation of Safety Critical Embedded Systems in Industrial Applications

The design and development of Safety-Critical Embedded Systems (SCES)is a relevant activity in many application fields such as railway, automotive, aerospace, health, etc. The life cycle of a new product must follow both regulatory constraints and challenging requirements and is continuously affected by a number of conflicting objectives to be achieved such as minimization of costs, improvement of performances, short time to market. Both service levels and deadlines of commitments must be satisfied without failing the required, more and more challenging, safety constraints. The Verification and validalidation represent a relevant phase that both discovers errors and certificates the achievement of the objectives. This thesis work aims to integrate into the Verification and Validation process of critical embedded systems methods to improve RAMS properties (Reliability, Availaility, Mantainability, Safety) of industrial application. We want to innovate the techniques used during the life-cycle for a railway system, in a world wide company, in order to verify and validate products in a shorter time and with the better results in terms of errors found and evidence of correctness about performed activities.