Skip to content

Latest commit

 

History

History
45 lines (24 loc) · 5.73 KB

socis.md

File metadata and controls

45 lines (24 loc) · 5.73 KB
Raw

Summer of Code in Space Proposal

The Summer of Code in Space (SOCIS, see sophia.estec.esa.int/socis/) opportunity for 2016 is focused on exploring the integration of the Overture toolset with the TASTE toolset (for more information see http://taste.tuxfamily.org). It is in line with the analysis presented in the paper presented at the 13th Overture workshop, which can be downloaded here: https://www.overturetool.org/workshops/13/MarcelVerhoef.pdf

We provide three possible opportunities for SOCIS students to work on. We encourage in particular students that wish to perform these activities as part of (or as precursor to) their thesis or diploma work.

The overture toolset currently supports a prototype code generator for the C-language. The objective of this project is to allow the automatic integration of this generated code into a piece of software comprising functions coded in other languages or using other code generators (such as Matlab-Simulink). The TASTE tools provide means to achieve this goal and need to be complemented with VDM-specific handling code.

In a TASTE system, functions can be implemented in a wide variety of languages. To make them communicate (i.e. function “hello” wants to call function “world” passing a parameter “foo” of a given type), TASTE relies on a language called ASN.1. ASN.1 provides a simple textual notation to define the exact content of the data types of the function parameters, in a way that is independent from specific implementation languages (C, Ada, Java..).

For example if the function “world” expects a parameter “foo”, we can define the type of “foo” like this:

TypeOfFoo ::= INTEGER (0..255)

ASN.1 supports a range of data types - both simple such as INTEGER, REAL, BOOLEAN and ENUMERATED, and complex such as SEQUENCE, CHOICE, SEQUENCE OF. Parameters of a record can be optional and other constraints can be applied.

What we want is to be able to implement the function “world” in either C or VDM, while the caller (“hello”) will be implemented in say, Ada or SDL.

If we had to do this manually, we would look at the “TypeOfFoo” type and find the best match in the VDM language to represent it (“nat”, most likely). Then we would look at how the VDM to C code generator works and in particular how it translates “nat” to a native C type (uint? int? etc.). We would do the same with the type used at the caller side, and make sure they fit. If not we would write a translating function: “from_TypeOfFoo_in_SDL_to_TypeOfFoo_in_VDM_C (...)”.

Despite being technically easy to perform, this is an error-prone and long process as soon as there are many functions to develop and maintain.

TASTE has tools that implements this whole process in an automated way: starting from the ASN.1 types it can (1) generate semantically-equivalent types in (virtually) any language, and (2) generate the translating functions at code level by knowing internally how third-party tools generate code.

The first part is called “A mappers” in TASTE terminology. In the scope of this project, the student will look at the preliminary work done here to translate ASN.1 to VDM : http://taste.tuxfamily.org/wiki/index.php?title=Work_in_progress:_Integrating_SDL_and_VDM and complete this A mapper. The result shall be a deterministic translation of all ASN.1-supported types to equivalent VDM types.

The second part is called “B mappers” and corresponds to the tools generating the translation functions at code level as described above. These mappers emit code that convert the data types obtained by the VDM to C code translator from and to the C data types generated by the ASN.1 compiler, as well as the piece of glue code that wraps the VDM function call with the translated parameter. The student will have to write this B-mapper for the VDM-to-C code generator. Example of B mappers are visible here: https://gitrepos.estec.esa.int/taste/dmt/tree/master/aadl2glueC

They are written in the Python language - the ASN.1 parser is built-in. The result shall be the possibility to generate object files for the VDM functions which are wrapped in a way that they can be called by any external function that “inherits” from the same ASN.1 data types.

A set of test cases shall be developed to demonstrate the results, covering all data types used by TASTE and expressed in the ASN.1 data model. The student should have commanding knowledge of VDM, C, and Python. Knowledge of ASN.1 is advantageous to perform this task. Note that an extendable and open source ASN.1 compiler and supporting run-time library is already available as part of the TASTE environment.

The idea would be to use this code generator to create combined SDL models (written with OpenGEODE, which is part of TASTE) and VDM models (written in Overture) that are deployed using the TASTE environment into a single working prototype. The challenge here is to allow seamless data exchange between the code generated from these models, which relies on ASN.1 in TASTE. A prototype of this approach (translating ASN.1 to VDM) is already available, see http://taste.tuxfamily.org/wiki/index.php?title=Work_in_progress:_Integrating_SDL_and_VDM. The work has the following objectives:

  • To provide a bi-directional ASN.1 binding for (a subset of) VDM datatypes, such that the c-code generated from the VDM models can be seamlessly integrated into TASTE to create working prototypes

  • To demonstrate this capability on a case study

  • To investigate (and prototype) the integration of an ASN.1 compliant communication capability directly in the Overture interpreter, which would allow the early integration of the Overture tool, rather than just the generated code from the models.

Mentor: Professor Peter Gorm Larsen (Aarhus University), co-mentor: Thanassis Tsiodras (ESA)