itemis offers consulting and engineering support for the mbeddr C open source project. mbeddr C is a new approach to embedded software development that integrates C, DSLs and formal verification. In particular, C can be extended with arbitrary domain-specific extensions, directly in the C code. By choosing suitable language abstractions, the program code becomes easily verifiable. mbeddr ships with a set of predefined extensions (incl. state machines, components and testing support) plus verifications for some of them (e.g. model checking for state machines).
Professional Support for mbeddr C
Itemis offers professional support for the open source mbeddr C technology stack, developed as part of the LW-ES research project. In particular, itemis will …
- help evaluating mbeddr
- support the adoption of mbeddr
- transfer knowledge about extending mbeddr
- build ready-to-use language extensions
… tailored to the needs of customers. Four of the core mbeddr contributors work for itemis. In addition, itemis cooperates with JetBrains and fortiss to provide full-spectrum support regarding mbeddr and MPS.
Please contact Kurt Ebert (see contact info on the right) for details.
About mbeddr C
mbeddr C is an extensible version of C, optimized for embedded programming, incl. an IDE, debugger and support for formal analyses. It is built on top of JetBrains MPS, an open source language workbench. Users can implement their own DSLs and language extensions based on the powerful language implementation and composition capabilities of MPS.
mbeddr comes with a set of default extensions ready to use in embedded software development. These include interfaces, components, state machines, unit test support as well as cross-cutting support for requirements tracing and product line variability.
Model Checkers and SAT solvers are integrated directly to support agile formal analyses, integrated into the development process and IDE. By default, state machines are checked for consistency, decision tables are checked for completeness and feature models and configurations are checked regarding freedom from conflicts.