Model Checking for Component-based Software Development for Embedded Systems

W. Maydl (Germany)


Dataflow-Based Embedded Systems, Model Checking, Design-Accompanying Analysis


Currently, testing is still the most time consuming part of software development for embedded systems. This be comes more and more problematic as size and complexity of embedded applications are continuously growing often combined with a decreasing time to market and cost reduc tion. To address this problem, a new model checking algo rithm for component-based design of dataflow-based em bedded systems is presented. This technique is based on a novel communication model of dataflow components. De pending on the computational complexity of the dataflow graph, either a complete analysis regarding deadlock de tection, memory usage and cyclic schedules is conducted or counter-examples may be detected in an early design phase. The state explosion problem is addressed by a new guided search strategy using several innovative tech niques which reduce time and memory consumption. Run time tests demonstrate the effectiveness of the algorithm for large dataflow graphs. This results in more reliable soft ware development of complex applications in a shorter de sign time.

Important Links:

Go Back