title = {Certifying Deadlock-freedom for BIP Models },
    author = {Blech, Jan Olaf and P'erin, Micha\"el},
    year = {2009},
    booktitle = {Software and Compilers for Embedded Systems (SCOPES)},
    team = {DCS,PACSS},
    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 propose the automatic generation of 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. The proof of deadlock-freedom fundamentally relies on the computation of invariant properties of the considered BIP model which is carried out by D-Finder and serves as basis for certificate generation. Encapsulating these invariants into certificates and checking them is the most important subtask of our methodology for guaranteeing deadlock-freedom.},

Contact | Site Map | Site powered by SPIP 4.2.13 + AHUNTSIC [CC License]

info visites 4004411