This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
Rigorous Component-Based System Design Using the BIP Framework
May/June 2011 (vol. 28 no. 3)
pp. 41-48
Ananda Basu, Verimag Laboratory
Saddek Bensalem, Verimag Laboratory
Marius Bozga, Verimag Laboratory
Jacques Combaz, Verimag Laboratory
Mohamad Jaber, Verimag Laboratory
Thanh-Hung Nguyen, Verimag Laboratory
Joseph Sifakis, Verimag Laboratory
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.

1. N. Halbwachs, Synchronous Programming of Reactive Systems, Kluwer Academic Publishers, 1993.
2. A. Burns and A. Welling, Real-Time Systems and Programming Languages, 3rd ed., Addison-Wesley, 2001.
3. S. Bliudze and J. Sifakis, "A Notion of Glue Expressiveness for Component-Based Systems," Proc. 19th Int'l Conf. Concurrency Theory (CONCUR 08), LNCS 5201, Springer, pp. 508–522.
4. S. Bliudze and J. Sifakis, "Causal Semantics for the Algebra of Connectors," Formal Methods in System Design, vol. 36, no. 2, 2010, pp. 167–194.
5. S. Bensalem et al., "Compositional Verification for Component-Based Systems and Application," Proc. 6th Int'l Symp. Automated Technology for Verification and Analysis (ATVA 08), LNCS 5311, Springer, 2008, pp. 64–79.
6. S. Bensalem et al., "Incremental Component-Based Construction and Verification Using Invariants," Proc. Formal Methods on Computer-Aided Design (FMCAD 10), Formal Methods in Computer-Aided Design, 2010, pp. 257–266; http://fmcad10.iaik.tugraz.at/PapersFMCAD10.pdf .
7. S. Bensalem et al., "D-Finder: A Tool for Compositional Deadlock Detection and Verification," Proc. 21st Int'l Conf. Computer Aided Verification (CAV 09), LNCS 5643, Springer, 2009, pp. 614–619.
8. B. Bonakdarpour et al., "From High-Level Component-Based Models to Distributed Implementations," Proc. 10th Int'l Conf. Embedded Software (EmSoft 10), ACM Press, 2010, pp. 209–281.
9. K.M. Chandy and J. Misra, Parallel Program Design: A Foundation, Addison-Wesley Longman, 1988.
10. R. Bagrodia, "Process Synchronization: Design and Performance Evaluation of Distributed Algorithms," IEEE Trans. Software Eng., vol. 15, no. 9, 1989, pp. 1053–1065.
11. S. Fleury, M. Herrb, and R. Chatila, "GenoM: A Tool for the Specification and the Implementation of Operating Modules in a Distributed Robot Architecture," Proc. 1997 IEEE/RSJ Int'l Conf. Intelligent Robots and Systems (IROS 97), IEEE Press, 1997, pp. 842–848.
12. A. Basu et al., "Incremental Component-Based Construction and Verification of a Robotic System," Proc. 18th European Conf. Artificial Intelligence (ECAI 08), IOS Press, 2008, pp. 631–635.
1. D. Garlan, R. Monroe, and D. Wile, "Acme: An Architecture Description Interchange Language, Proc. 1997 Conf. Centre for Advanced Studies on Collaborative Research (CASCON 97), IBM Press, 1997, pp. 169–183.
2. J. Magee and J. Kramer, "Dynamic Structure in Software Architectures," Proc. 4th ACM SIGSOFT Symp. Foundations of Software Eng. (SIGSOFT 96), ACM Press, 1996, pp. 3–14.
3. OMG Systems Modeling Language SysML (OMG SysML), v. 1.2, Object Management Group, 2010; www.omg.org/spec/SysML/1.2.
4. P.H. Feiler, B. Lewis, and S. Vestal, "The SAE Architecture Analysis and Design Language (AADL): A Standard for Engineering Performance Critical Systems," IEEE Conf. Computer Aided Control Systems Design (CACSD 06), IEEE Press, 2006, pp. 1206–1211.
5. J. Eker et al., "Taming Heterogeneity: The Ptolemy Approach," Proc. IEEE, vol. 91, no. 1, 2003, pp. 127–144.

Index Terms:
component-based design, model-based design, design flow, model transformation, correctness, invariant generation, deadlock-freedom, code generation, autonomous robots
Citation:
Ananda Basu, Saddek Bensalem, Marius Bozga, Jacques Combaz, Mohamad Jaber, Thanh-Hung Nguyen, Joseph Sifakis, "Rigorous Component-Based System Design Using the BIP Framework," IEEE Software, vol. 28, no. 3, pp. 41-48, May-June 2011, doi:10.1109/MS.2011.27
Usage of this product signifies your acceptance of the Terms of Use.