Verimag

The BIP Design Flow

The Rigorous Design Flow

The BIP design flow uses a single language (BIP) which makes possible a rigorous checking of the consistency between the different design steps. Rigorousness is primarily ensured by applying source-to-source transformations between refined systems models. By application of compositionality rules, we show that transformations preserve observational equivalence (and consequently essential safety properties). Verification is applied only to high level models for checking safety properties such as invariants and deadlock-freedom. To avoid inherent complexity limitations, the verification method applies compositionality techniques efficiently implemented by using heuristics in the D-Finder tool.

The design flow involves 4 distinct steps:

  1. The translation of the application software into a BIP model. This allows its representation in a rigorous semantic framework. There exist translations of several programming models into BIP including synchronous, data-flow and event driven models.
  2. The generation of an abstract system model from the BIP model representing the application software, a model of the target execution platform as well as a mapping of the atomic components of the application software model into processing elements of the platform. The obtained model takes into account hardware architecture constraints and execution times of atomic actions. Architecture constraints include mutual exclusion induced from sharing physical resources such as buses, memories and processors as well as scheduling policies seeking optimal use of these resources.
  3. The generation of a concrete system model obtained from the abstract model by expressing high level coordination mechanisms e.g. interactions and priorities by using primitives of the execution platform. This transformation usually involves the replacement of atomic multiparty interactions by protocols using asynchronous message passing (send/receive primitives) and arbiters ensuring overall coherency e.g. non interference of protocols implementing different interactions.
  4. The generation of monolithic C code from sets of interaction components executed by the same processing unit. This transformation allows efficient implementation by avoiding overhead due to coordination between components.

Contact | Site Map | Site created with SPIP 2.1.26 + AHUNTSIC [CC License]

Logged in visitors: 6 ; visits: 448518