Rigorous Component-Based System Design Using the BIP Framework

被引:166
作者
Basu, Ananda
Bensalem, Saddek
Bozga, Marius
Combaz, Jacques
Jaber, Mohamad
Thanh-Hung Nguyen
Sifakis, Joseph
机构
关键词
VERIFICATION;
D O I
10.1109/MS.2011.27
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
Rigorous system design requires the use of a single powerful component framework allowing the representation of the designed system at different detail levels, from application software to its implementation. A single framework allows the maintenance of the overall coherency and correctness by comparing different architectural solutions and their properties. The authors present the BIP (behavior, interaction, priority) component framework, which encompasses an expressive notion of composition for heterogeneous components by combining interactions and priorities. This allows description at different abstraction levels from application software to mixed hardware/software systems. A rigorous design flow that uses BIP as a unifying semantic model derives a correct implementation from an application software, a model of the target architecture, and a mapping. Implementation correctness is ensured by applying source-to-source transformations that preserve correctness of essential design properties. The design is fully automated and supported by a toolset including a compiler, the D-Finder verification tool, and model transformers. The authors present an autonomous robot case study to illustrate BIP's use as a modeling formalism as well as crucial aspects of the design flow for ensuring correctness. © 2011 IEEE.
引用
收藏
页码:41 / 48
页数:8
相关论文
共 12 条