If Fomal Analysis is the Answer – What was the Question?

A key challenge of implementing an embedded systems application on a heterogeneous multiprocessor SoC platform is to find the right mapping of the application onto the platform architecture. The right mapping is dependent on the characteristics of the processors and the network connecting them, as well as the application. As many embedded systems are heavily resource constrained and often safty-critical, there is a strong desire to be able to reason about properties of the system. Although the classical approach of simulation may help us in gaining confidence, it will never be able to make guarantees. However, formal models have promises of being able to give such guarantees – but, can we formally model complex MPSoC systems? And if so, what kind of system properties can we expect to be able to formally verify?