Model based Design and Validation of the hybrid Model

Demonstrate improved applicability of the formal verification approaches, providing formal guarantees on the stability of the control system with symbolic techniques.

Short Description

The tool Sabbath is applied to a real-world problem. The model considered is a hybrid system of 21 real variables with two modes, each one consisting of an affine dynamical system. Sabbath is integrated into an ad-hoc script that consecutively executes the following tasks: • Reformulation of the closed loop with PI controllers as switched affine system; • Find candidate quadratic Lyapunov functions for each mode of the hybrid system; • Certificate the validity of the candidate Lyapunov functions; • Synthesis and validation of a region for which stability is proved; • Synthesis of a robust region for reference values. The main programming language is Python, and we make use of several modules to validate the results. The versatility of SMT solvers plays an important role since they adapt with ease to hybrid systems problems.

Use cases

Responsible(s)/Contact(s)

TRL

Demonstrator Evaluation Criterias

Highlights/Rationale of the demonstrator

Transferability Comment Transferability defines how easily the technology can be applied in different systems or areas.

Transferability level 1-Minor, 2-Fair, 3-Good , 4-Very good , 5-Excellent (Minor: The purpose of the technology is connected to a specific system. It is hardly possible or even impossible to adopt the Technology in different systems. Fair: The technology is strongly coupled with another technology that is limited to be used elsewhere (e.g., due to licensing). Good: The technology is developed for a specific purpose but enables modifications to be applied elsewhere. Some specifics must be taken into consideration while adopting it. Very good: The technology is not purpose specific and can be applied elsewhere with small modifications. Excellent: The technology is general, implements standard interfaces, or has already been used in different areas with no or minor modifications.)

Improvement Level 1-Minor, 2-Fair, 3-Good , 4-Very good , 5-Excellent

Demonstrator Result/Measurement of V&V process Improvement List of V&V process improvement measurement based on VALU3S Evaluation Criterias per Use case Test Case and requirement

Demonstrator Result/Measurement of V&V SCP Improvement List of V&V of SCP improvement based on VALU3S Evaluation Criterias per Use case Test Case and requirement

Link to use cases

Qualitative Results

Qualitative Evaluation results obtained through QAM

Demonstrator pitch video Demonstrator pitch video hosted in VALU3S youtube channel

Contents

UC5 Mapping-2-18 EvalCriteriaV&V-1

Evaluation of volume of synthesized stable region and of robustness to parameter changes via multiple methods.

UC5 Mapping-2-18 EvalCriteriaV&V-3

Evaluation of volume of synthesized stable region and of robustness to parameter changes via multiple methods.

Qualitative Evaluation results obtained through QAM