Integrating Architectural Constraints in Application Software by Using Model Transformations in BIP

A. Basu, S. Bensalem, P. Bourgos, M. Bozga, and J. Sifakis
Invited presentation at IEEE International High Level Design Validation and Test Workshop, Anaheim, USA, 2010
Performance of embedded applications strongly depends on features of the hardware platform on which they are deployed. A grand challenge in the design of complex embedded systems is developing methods and tools for modelling and analysing the behaviour of an application software running on a given hardware architecture. We propose a rigorous method that allows to obtain a model which faithfully represents the behavior of a mixed hardware/software system from a model of its application software and a model of its underlying hardware architecture. The method takes a model of the application software in BIP, a model of the hardware architecture in XML and a mapping associating read and write operations of the application software with execution paths in the architecture. It builds a model of the corresponding system in BIP. The latter can be simulated and analysed for the verificationcation of both functional and extra-functional properties. The method consists in progressively enriching the application software model. It involves two steps: (1) The identification of the a set of hardware components used in the system model. These are included in the initial model. They are obtained by a systematic decomposition of the architecture through an abstract grammar. (2) The application of a sequence of source-to-source transformations to synthesize run-time routines implementing software channels. The transformations are correct-by-construction. In particular they preserve functional properties of the application software. We have identified a minimal and complete set of transformation rules, that are proved to be correct. The system model is highly parametrized and allows flexible integration of specific target architecture features, such as bus policy and scheduling policy of the processor cores. The method has been implemented for software applications and hardware architectures described in the DOL tool for performance evaluation. We plan to test benchmark applications on a simplified MPARM architecture.