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:
- Code generation for simulation/validation on a linux PC
- Functional correctness using the D-Finder tool, checking for deadlocks
- Transformations for code generation that uses send/receive primitives, for execution on distributed architectures.
- Performance analysis (e.g. latency), based on simulation and statistical model checking facility integrated with BIP.
This work was part of the PRO3D project.