FP7Индивидуална стипендия2008–2010

DYNAGALS · Formal design methods for globally asynchronous/locally synchronous embedded computing systems

7РП — „Хора“ (Действия „Мария Кюри“)

Период
2008-03-01 → 2010-02-28
Финансиране от ЕС
111 667 €
Участници
1
Схема
MC-IOF

Линиите свързват координатора с партньорите.

Накратко на български

Методите за проектиране на сложни вградени системи, като чипове със стотици ядра, се изследват чрез езика SystemJ. Това помага за преодоляване на разликата между нарастващата сложност на хардуера и софтуера, който работи върху него.

Този кратък обзор е генериран от изкуствен интелект

Кратко обяснение, генерирано от езиков модел по текста на CORDIS. Оригиналът е по-долу.

Резултати накратко

Formal design methods for globally asynchronous/locally synchronous embedded computing systems

The focus of the DYNAGALS project was to propose novel and formal approaches to tackle the design-productivity gap existing in the field of complex and heterogeneous embedded computing systems. This gap arises from two facts: first, embedded processors are becoming more and more complex (future many-core chips will incorporate 100 cores with a NoC, a complex memory hierarchy, dynamic voltage and frequency scaling islands, ...), and second, applications running on those processors are becoming ever larger, with more and more complex and heterogeneous features. The four contributions of the DYNAGALS project to the reduction of the design-productivity gap belong to the domains of high-level programming languages, time-predictability, and component-based design. 1. We worked on the SystemJ programming language. SystemJ combines the data processing and encapsulation elegance of Java with with the reactivity and synchrony of Esterel and the asynchronous decoupling of CSP. Hence, SystemJ is a programming language particularly suited to the design of globally asynchronous locally synchronous systems (GALS). We specified the formal semantics of the language and its runtime support, and designed a novel multi-core architecture, consisting of two kinds of computing cores and an interconnection fabric for the communications and synchronizations between those cores. We designed two compilers, one that produces multi-threaded Java code to be executed on a regular Java virtual machine, and another that produces hardware/software embedded code for the above-mentioned multi-core architecture. We also conducted several case studies to evaluate the practical usefulness of SystemJ for the design of embedded systems. 2. We proposed a dynamic extension of SystemJ, called DSystemJ, aimed at the design of dynamic distributed GALS systems. It addresses the issue of adaptivity in distributed systems, by providing the ability to create and fork dynamically new processes, to change dynamically the communication topology between the processes, and to migrate processes from one location to another. Typical applications include sensor networks. For instance, a case study has been conducted for a video monitoring system, where new cameras - and their controlling software - can be added at run-time. 3. We designed a new time-predictive programming language, called Pret_C, based on the C programming language (the most widely used language for programming embedded systems), extended with several constructs to support synchronous concurrency, preemption, and logical time at a high-level. In contrast to existing synchronous languages, Pret_C offers C-based shared memory communications between concurrent threads that is guaranteed to be thread safe. Thanks to the synchronous semantics that we proposed, the mapping of logical time to physical time can be achieved much more easily than with plain C. We also designed a dedicated target architecture, called ArPret, which combines a hardware accelerator associated to an existing soft core processor. It allowed us to improve the throughput of Pret_C programs while preserving the predictability. 4. We worked on the topic of converter synthesis for component-based systems. Component-based design is a paradigm where complex systems are built incrementally from small encapsulated blocks of code called components. The main problem raised by this approach is that only the communication interface of each component is known, and that assembling components often results in control, data, and clock mismatches. Converter synthesis amounts to synthesising, as automatically as possible, a converter to bridge the mismatches between interacting components. Within the DYNAGALS project, we proposed a new formal approach to solve this, problem, and we are the first able to handle the three kinds of potential mismatches in a unified way.

Текст от CORDIS, на английски · Данни: CORDIS, © Европейски съюз

Цел на проекта

We propose a novel approach to tackle the design-productivity gap existing in the field of complex and heterogeneous embedded computing systems. We take as a starting point the SystemJ programming language, which combines the data processing and encapsulation elegance of Java with with the reactivity and synchrony of Esterel and the asynchronous decoupling of CSP (that is, with rendezvous communications). Our research proposal aims at improving SystemJ in two directions: first for the formal verification of SystemJ programs, and second for the automatic synthesis of hardware/software embedded code. An implementation within a complete tool is also planned. These two goals will help SystemJ becoming one of the leading system-level design language for complex and heterogeneous embedded systems. The first goal (formal verification) is essential for the validation of the system under design. As embedded computing systems are often safety-critical, formal verification is a crucial feature for a system-level design tool. We shall use observer-based model-checking, with state-space reduction techniques. The second goal (code synthesis) is crucial too because it avoids the tedious and error-prone phase of manual coding from the high-level specification. Instead, we shall be able to generate automatically a mixed hardware and software implementation, proven to be faithful to the high-level specification written in SystemJ. Such a proof of faithfulness shall be based on the formal semantics of SystemJ. These scientific research results shall be implemented within a tool suite, and we shall conduct case studies to evaluate its practical usefulness for the design of embedded systems as well as its performances.

Оригинален текст от CORDIS (на английски).

Участници

  • INSTITUT NATIONAL DE RECHERCHE EN INFORMATIQUE ET AUTOMATIQUE · Le Chesnay CedexКоординаторФранция

Връзки

Данни: CORDIS, © Европейски съюз