VeriStab · Formal Verification of Stability of Embedded Control Systems
7РП — „Хора“ (Действия „Мария Кюри“)
- Период
- 2014-03-01 → 2018-02-28
- Финансиране от ЕС
- 100 000 €
- Участници
- 1
- Схема
- MC-CIG
Линиите свързват координатора с партньорите.
Накратко на български
Вградените системи за управление се анализират чрез автоматизирани методи, за да се гарантира, че малки смущения в началото няма да доведат до големи отклонения в работата им. Това предотвратява критични повреди и катастрофални последствия при експлоатацията на тези системи.
Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.
Резултати накратко
Formal Verification of Stability of Embedded Control Systems
Building high confidence embedded control systems is a grand challenge today. A fundamental property expected out of every control system design is stability, which captures the notion that small perturbations in the initial state or input to the system result in only small variations in the eventual behavior of the system. Systems which do not possess this property are operationally critical and could lead to catastrophic consequences. The main goal of the project was to develop automated formal techniques for verifying stability of embedded control systems. The project developed a novel approach for stability verification that applied model-checking, a successful verification paradigm from the formal methods field, to stability verification. In contrast to existing techniques which are deductive, the approach taken in the project was algorithmic. This facilitated the development of fully automated and scalable methods for stability verification, thereby addressing the shortcomings of the state-of-the-art deductive techniques. The specific technical results of the project include: [1] Quantitative predicate abstractions were proposed which constructed finite state abstraction with quantitative information to reason about the stability [2] A software tool AVERIST has been developed as part of the project, and is made publicly available for other researchers and engineers to use for stability analysis More information can be found at the dedicated Project's web page: http://software.imdea.org/projects/averist/index.html
Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз
Цел на проекта
Building high confidence embedded control systems is a grand challenge today. A fundamental property expected out of every control system design is stability, which captures the notion that small perturbations in the initial state or input to the system result in only small variations in the eventual behavior of the system. Systems which do not possess this property are operationally critical and could lead to catastrophic consequences. The main goal of the project is to develop automated formal techniques for verifying stability of embedded control systems.The project proposes a novel approach for stability verification - the application of model-checking, a successful verification paradigm from the formal methods field, to stability verification. In contrast to existing techniques which are deductive, the approach taken in the project is algorithmic. This will facilitate the development of fully automated and scalable methods for stability verification, thereby addressing the shortcomings of the state-of-the-art deductive techniques.An algorithmic approach to stability verification is a challenging task, since, even fundamental notions for abstraction and composition, which form the backbone of scalable algorithmic verification, have not been well explored. In this project, we propose a three phase plan from developing theoretical foundations to algorithm design and software tool development.
Оригинален текст от CORDIS (на английски).
Участници
- FUNDACION IMDEA SOFTWARE · Pozuelo De AlarconКоординаторИспания
Връзки
Данни: CORDIS, © Европейски съюз