LOLAES · Logical languages for embedded systems
6РП — Действия „Мария Кюри“
- Период
- 2007-01-01 → 2007-12-31
- Финансиране от ЕС
- 46 990 €
- Участници
- 1
- Схема
- EIF
Линиите свързват координатора с партньорите.
Накратко на български
Вградените системи, като тези в спирачките на автомобилите или управлението на самолети, се анализират чрез математически модели и логически езици. Това помага на инженерите да създават по-надеждни системи с доказано правилно функциониране.
Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.
Резултати накратко
Final Activity Report Summary - LOLAES (Logical Languages for Embedded Systems)
Embedded systems are becoming increasingly prevalent in daily life; for example, they appear in car braking systems, mobile phones, aircraft flight control systems, washing machines, etc. Correspondingly, the design of such systems is becoming increasingly complex and challenging. The aim of this project was to devise fundamental frameworks and algorithms for reasoning about the correct functioning of embedded systems. The approach we have followed falls under the broad umbrella of 'Model Checking'; it consists in representing the specification of a given system in a mathematical formalism known as temporal logic, and verifying whether a given model of the system meets its specification. To this end, we have developed new specialised temporal logic specification formalisms designed specifically to handle the precise timing and probabilistic aspects of the systems under consideration. Moreover, we have developed efficient algorithms for model-checking such specifications, and have begun prototype implementations of our algorithms. In the long run, our work should enable engineers to have increased confidence in their designs and ultimately produce provably correct systems.
Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз
Цел на проекта
Embedded systems are a modern technology, which has a large impact on the daily life. One of the characteristics of these systems is that they have to meet numerous quantitative constraints, like resource constraints (power consumption, memory usage, costs, bandwidth, etc...), timed constraints (response time, propagation delays, etc...), and constraints on the environment in which it operates (signal sensors, continuous evolution of the environment, open systems, etc...).Another important characteristic of embedded systems is that they have to be powerful and reliable. Their conception and verification thus pose a great challenge. The research project we propose to achieve concerns logical languages for describing correctness and safety properties of embedded systems, and in particular logical languages taking into account timed constraints and resource consumption constraints of the system. These logics have been considered in the early 90's and are now reconsidered, thanks to a recent result by J. Ouaknine and J. Worrell, which states that they can be used for verification purpose. Our research plan is structured on three main axes. The first one consists in developing a deeper understanding of automata-based properties of linear-time timed temporal logics. The second one consists in considering quantitative extensions of these formalisms with cost information and/or probabilities. The last one concerns the verification of programs using the game semantics approach.This program research is part of one of the strategic objectives of the research priority and Information Society Technologies" (embedded systems). This proposal is aimed at building a new collaboration between an EU researcher and an EU institution having common research motivations, though not exactly the same techniques and points of view."
Оригинален текст от CORDIS (на английски).
Участници
- THE CHANCELLOR, MASTERS AND SCHOLARS OF THE UNIVERSITY OF OXFORD · OXFORDКоординаторОбединеното кралство
Връзки
Данни: CORDIS, © Европейски съюз