DYNAGALS

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

 Partecipanti

Mappa

 Word cloud

Esplora la "nuvola delle parole (Word Cloud) per avere un'idea di massima del progetto.

 Obiettivo del progetto (Objective)

'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.'

Introduzione (Teaser)

A gap exists between the design and productivity of complex and heterogeneous embedded computing systems. A European project is looking to close this gap through a set of formal methods and programming languages developed over 24 months.

Descrizione progetto (Article)

Heterogeneous computing systems are basically electronic systems that run different computational units (such as audio or video systems, networked applications, etc.) and need extra specialised resources to work.

The design-productivity gap in these systems occurs for two main reasons: embedded processors are becoming more complex and the applications running on these processors are larger and equally complex. As a result, the DynaGALS project looked at three issues to overcome these problems: high-level programming languages, time-predictability, and component-based design.

To tackle the first concern, the researchers looked at the SystemJ programming language. SystemJ is particularly suited to the design of globally asynchronous locally synchronous systems (GALS), a crucial part of the project. DynaGALS set about defining the task and conducted case studies to see whether SystemJ could be used for the design of embedded computing systems.

Secondly, the team created a new time-predictive programming language, called Precision Timed C (Pret_C). This is based on the widely used C programming language with some added dynamics to improve performance. Pret C allows memory communication between two existing threads, something normal C programming does not offer. As a result, the mapping of logical time to physical time was more easily achieved. Arpret, a dedicated target architecture combining a hardware accelerator with a soft core processor which increased the efficiency of Pret_C, was also designed.

The third issue that DynaGALS tackled had to do with component-based systems. These are complex systems that are made of blocks of code or components. An essential problem is how to compose components designed in isolation when only the communication interface of an individual component is known.

When you try to link the different components together, regular mismatches occur. As a result, the team created a new formal approach incorporating a converter synthesis (a type of verification) which bridged the mismatches between different components.

The project, which cost EUR 111,667, ran until February 2010. SystemJ promises to become the major system-level design language for complex and heterogeneous embedded systems.