Written by Federico Tomassetti
in Jetbrains MPS

    Currently I am in Munich, working at Fortiss, an institute of the Technische Universität München. I am here to work on mbeddr, which is a super-cool project.

    mbeddr supports embedded software development based on an extensible
    version of C language and IDE. Existing extensions include interfaces with pre- and postconditions, components, state machines and physical units, as well as support for requirements tracing and product line variability. Based on these abstractions, mbeddr also supports formal verification based on model checking and SMT solving.

    What it means in practice?

    We are using a Jetbrains MPS to build an extensible variant of C. Using mbeddr the user could write plain C code and use, when it is needed, some extra features.

    One example? State machines. Instead of manually encoding them using a bunch of switch the user could use specific constructs. Some advantages:

    • it is less error prone,
    • it is faster,
    • the editor understand what you are doing and catch your errors,
    • you can verify that some properties holds (e.g., are all the states reachable?)

    In other words mbeddr permits to work to higher levels of abstractions.

    How C and mbeddr-C differs

    Mbeddr supports almost all the features of C. It does not support error-prone features like the preprocessor. For most of the usages of the preprocessor mbeddr offers higher-level constructs. Consider for example variability. In C you would see this code:

    void foo(){
      init();
    #if SOME_FEATURE_IS_ENABLED && VERSION>3
      // do great things!
    #elif SOME_FEATURE_IS_ENABLED
      // do less great things
    #else
      // do almost nothing
    #endif
      printResults();
    }
    

    In mbeddr-C you would write something like:

    Variability in mbeddr

    in practice you have the possibility to decorate statements and functions with their presence condition. This is cool for many reasons, first of all the possibility for mbeddr to verify that your code is valid under every possible configuration.

    What is my contribution?

    I am building the importer which converts plain C to mbeddr-C. It interprets how the preprocessor is used in C code and translate it to higher level concepts.

    In this video I show the current state of the importer.

    If you want some more details about the importer you can read this very preliminary paper, accepted for the Reverse Engineering workshop to be held in Genova on the 5th of March.

    Download the guide with 68 resources on Creating Programming Languages

    Receive the guide to your inbox to read it on all your devices when you have time

    Powered by ConvertKit
     
    Creating a Programming Language

    Learn to Create Programming Languages

    Subscribe to our newsletter to get the FREE email course that teaches you how to create a programming language