Certifying deadlock-freedom for BIP models
Jan Olaf Blech, Michaël Périn · 2009
The BIP framework provides a methodology supported by a tool chain for developing software for embedded systems. The design of a BIP system follows the decomposition in behavior, interaction and priority. The first step comprises the division of desired behavior of a system into components. In a second step interactions and their priorities are added between the components. Finally, machine code is generated from the BIP model. While adding interactions it is possible to overconstrain a system resulting in potential deadlocks. The tool chain crucially depends on an automatic tool, D-Finder, which checks for deadlock-freedom.