Verimag

Language Factory

Generating BIP Models from Other Languages

The Language Factory activity concerns the use of BIP as an unifying semantic model for structural representation of such different programming models or domain specific languages. We have developed a general method for generating BIP models from languages with well-defined operational semantics.

Overview

Hardware/Software components are commonly designed and implemented according to programming models and/or using domain specific languages.

The Language Factory activity concerns the use of BIP as an unifying semantic model for structural representation of such different programming models or domain specific languages.

We have developed a general method for generating BIP models from languages with well-defined operational semantics. As depicted in the figure above, the method involves the following three steps for a given application software written in a language L:

  • Translation of atomic components of the source language into BIP components. The translation focuses on the definition of adequate interfaces. It encapsulates and reuses data structures and functions of the application software,
  • Translation of coordination mechanisms between components of the application software into connectors and priorities in the target BIP model,
  • Generation of a BIP component modeling the operational semantics of L. This component plays the role of an engine coordinating the execution of the application software components.

This three step transformation from a language L to BIP have been successfully tested for:


Synchronous Systems in BIP

We provide in [1] a general representation for the synchronous programming model. We show that we can meaningfully represent synchronous components e.g., Lustre nodes, using (compositions of) atomic components with a particular cyclic behavior. This representation reveals in BIP the least coordination required for the correct execution of synchronous systems. Moreover, for this particular class of components we provide sufficient syntactic conditions to ensure deadlock freedom and confluence of computations.

contact: Marius Bozga


MATLAB/Simulink to BIP

MATLAB/Simulink is a very popular commercial tool for model-based design and simulation of dynamic embedded systems. Simulink is widely used by engineers since it provides a wide variety of block libraries for implementing and testing discrete and continuous systems occurring in many application domains.

We are developing a method for the translation of a discrete-time fragment of Simulink into the synchronous subset of the BIP language. The translation presented in [2] is fully compositional, that is, it preserves completely the original structure and reveals the minimal control coordination structure needed to perform the correct computation within Simulink models. Additionally, this translation can be seen as providing an alternative operational semantics of Simulink models using BIP.

contact: Marius Bozga


AADL to BIP

The paper [3]. presents a general methodology and an associated tool for the structural translation of AADL specifications into BIP. In this work, we define precise operational models for all AADL components in terms of BIP components. Moreover, we clearly define the AADL communication mechanisms using various types of ports in terms of BIP interaction models. This precise mapping enables simulation of systems specified in AADL as well as their analysis using formal verification techniques developed for BIP, e.g. deadlock detection.

contact: Marius Bozga


GeNoM to BIP

GeNoM is a C++ software framework used for the implementation of the functional layer within autonomous robotic applications. Our joint collaboration with LAAS reported in [4], [5] demonstrates that BIP can be seamlessly integrated within the preexisting design methodology, in particular:

  • BIP has been used for (1) the incremental modeling of GenoM modules used to implement the functional level and (2) the modeling of their allowed interactions as specified by the control execution level of the robot;
  • the resulting BIP model has been used to synthesize a controller for the overall execution of all the functional modules and to enforce by construction the constraints and the rules inside modules but also between the various functional modules;
  • the BIP model has been also used to formally verify several safety-critical properties of the robot including ordering and synchronization constraints, data freshness properties, deadlock-freedom, etc.

contact: Saddek Bensalem


NesC/TinyOS in BIP

In [6], we present a compositional methodology for modeling and analyzing sensor network applications using BIP. For every sensor, its model consists of a composition of (1) a model extracted from a nesC program describing the application, and (2) an abstract models of TinyOS components. This opens the way for enhanced analysis and early error detection by using verifications techniques.

contact: Ananda Basu


C to BIP

We provide a translation process from any C code to a BIP model. The translator accepts any C code as input and currently support a reasonable subset of the C language. Any C function can be translated to a BIP atomic component. A set of function are considered as interaction points and all corresponding calls are modeled by BIP ports. This translation is used as a building block for other factories (MIND project and DOL)

contact: Marc Poulhiès


DOL to BIP

We present a rigorous method that allows to obtain a system model which faithfully represents the behavior of a mixed hardware/software system from a model of its Application Software, a model of its underlying Hardware Architecture, and a given Mapping. DOL is used as a frontend for describing the Application Software (in C), the Harware Architecture (in XML), and the Mapping (in XML). We have implementing a tool that takes DOL description and generates a system model in BIP. The tool uses C to BIP to translate Application Software (C) into BIP Software model.

The system model can be simulated and analyzed for the verification of both functional and extra-functional properties, using the BIP toolset, such as:

  1. Code generation for simulation/validation on a linux PC
  2. Functional correctness using the D-Finder tool, checking for deadlocks
  3. Transformations for code generation that uses send/receive primitives, for execution on distributed architectures.
  4. Performance analysis (e.g. latency), based on simulation and statistical model checking facility integrated with BIP.

This work is part of the PRO3D project.

contact: Ananda Basu

[1M. Bozga, V. Sfyrla and J. Sifakis. Modeling Synchronous Systems in BIP. In Embedded Software EMSOFT’09 Proceedings

[2V. Sfyrla, G. Tsiligiannis, I. Safaka, M. Bozga and J. Sifakis Compositional Translation of Simulink Models into Synchronous BIP. In Symposium on Industrial Embedded Systems SIES’10 Proceedings, WIP track.

[3Y. Chkouri, A. Robert, M. Bozga and J. Sifakis Translating AADL into BIP - Application to the Verification of Real-Time Systems In Model-Based Architecting and Construction of Embedded Systems ACES MB’08 Workshop Proceedings

[4S. Bensalem, F. Ingrand and J. Sifakis. Autonomous Robot Software Design Challenge. In 6th IARP/IEEE-RAS/EURON Joint Workshop on Technical Challenge for Dependable Robots in Human Environments, 2008

[5A. Basu, M. Gallien, C. Lesire, T. Nguyen, S. Bensalem, F. Ingrand and J. Sifakis. Incremental Component-Based Construction and Verification of a Robotic System. In European Conference on Artificial Intelligence ECAI’08 Proceedings, volume 178 of FAIA, pages 631-635, IOS Press

[6A. Basu, L. Mounier, M. Poulhiès, J. Pulou and J. Sifakis. Using BIP for Modeling and Verification of Networked Systems - A Case Study on TinyOS-based Networks. In Sixth IEEE International Symposium on Network Computing and Applications (NCA 2007) Proceedings, pages 257-260.


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

info visites 670854