In safety-critical areas, model-based software engineering or software development has gradually entered the equipment development process in my country. Using embedded software modeling tools such as SimuLink or SCADE to visually model algorithms or control logic, and then generate highly reliable binary codes has gradually become the mainstream software development method in safety-critical fields.
The ModelCoder independently developed by our company is a software design and development tool that supports modeling of a variety of embedded systems and can automatically generate highly secure and reliable C code. ModelCoder supports embedded models such as synchronous data streams and state machines. The process of generating code from the model has undergone formal verification to ensure the correctness of the generation process. It can be used for aircraft flight control, aircraft avionics, and nuclear power. Design and development of embedded software in multiple safety-critical fields such as DCS.
Principle of ModelCoder
The code generation tool is a kind of compiler, which translates the model language into C language. Code generation tools are widely used in my country's aviation, rail transit and nuclear power and other safety-critical fields.
Ensuring the safety and reliability of the generation process of code generation tools is a subject that must be faced in safety-critical areas. ModelCoder adopts the most rigorous formal technology, using theorem proof method to carry out rigorous mathematical proof of the model-to-code generation process. Compared with KCG of the similar software SCADE, KCG only uses model checking technology to prove the model itself, and ModelCoder is undoubtedly more reliable in terms of technical approaches.
The translation process of ModelCoder is as follows:
▲Figure-1: ModelCoder translation process diagram
Features of ModelCoder
The function of ModelCoder is divided into three parts:
Graphical software modeling: use intuitive graphic symbols to build a data flow model;
Simulation test: Based on the automatically generated C code to simulate the running process of each module, design defects can be found early;
Automatic code generation: The model language is used to formally generate reliable C code automatically.
▲Figure-2: Graphical front end of ModelCoder
▲Figure-3: ModelCoder's simulation running test module
Specific operators are used to support specific data structures, for example, Map is used to support operations on Array;
Control the complexity of the module and minimize the call of sub-modules. Every time the generated code calls a function, the overhead of function parameter transfer will occur. At this time, if there are more loops in the upper layer, the cost of parameter transfer will be higher;
Check duplicate modules and merge duplicate items as much as possible to form a basic library;
The gate circuit should be optimized before modeling, which can reduce the complexity of the model;
Control the number of local variables and reduce unnecessary local variables to prevent additional stack creation and destruction overhead.