Jan Olaf Blech, Michaël Périn
On Certificate Generation and Checking for Deadlock-freedom of BIP Models (2008)
On Certificate Generation and Checking for Deadlock-freedom of BIP Models (2008)
TR-2008-19.pdf
Keywords: certificate generation, invariants, theorem proving, Coq
Abstract: 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. This paper reports on guaranteeing the correctness of the verdict of D-Finder. We address the problem of formally proving deadlock-freedom of an embedded system in a way that is comprehensible for third party users and other tools. We achieve this goal by automatically generating certificates for each BIP model declared safe by D-Finder. These certificates comprise a proof of deadlock-freedom of the BIP model which can be checked by an independent checker. We use the Coq theorem prover as certificate checker. Thus, bringing the high level of confidence of a formal proof to the deadlock analysis results. With the help of certificates one gets a deadlock-freedom guarantee of BIP models without having to trust or even take a look at the deadlock checking tool. Part of the proofs encapsulated in certificates are invariants of considered BIP models. Their checking is an important subtask to guarantee deadlock-freedom of the given BIP model.
