Model–Based Analysis Tools for Component Synthesis

  • Luigia Petre
  • Kaisa Sere
  • Leonidas Tsiopoulos
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 6957)


Component-based development typically refers to assembling pre-existing pieces of software or hardware for integrating them into new systems. In this paper we introduce a formalism-based approach to verify the component boundaries, based on the component interdependencies. We base this synthesis method on B Action Systems and the animation techniques provided by the ProB tool. In addition, we put forward another applicability for our method, namely to mapping components to hardware platform tiles.


Component Synthesis B Action Systems ProB tool Application Mapping 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Dellarocas, C.: The SYNTHESIS Environment for Component-Based Software Development. In: 8th International Workshop on Software Technology and Engineering Practice (STEP 1997), p. 434 (1997)Google Scholar
  2. 2.
    Szyperski, C.: Component Software - Beyond Object-Oriented Programming. Addison-Wesley, ACM Press (1998)Google Scholar
  3. 3.
    Lecomte, T.: Safe and Reliable Metro Platform Screen Doors Control/Command Systems. In: Cuellar, J., Sere, K. (eds.) FM 2008. LNCS, vol. 5014, pp. 430–434. Springer, Heidelberg (2008)CrossRefGoogle Scholar
  4. 4.
    Bernardo, M., Cimatti, A. (eds.): SFM 2006. LNCS, vol. 3965. Springer, Heidelberg (2006)Google Scholar
  5. 5.
    Waldén, M., Sere, K.: Reasoning about Action Systems using the B Method. Formal methods in System Design 13(1), 5–35 (1998)CrossRefGoogle Scholar
  6. 6.
    Abrial, J.-R.: The B–Book. Cambridge University Press, Cambridge (1996)CrossRefzbMATHGoogle Scholar
  7. 7.
    Leuschel, M., Butler, M.: ProB: A Model Checker for B. In: International Symposium of Formal Methods Europe, pp. 855–874 (2003)Google Scholar
  8. 8.
    Bert, D., Potet, M.-L., Stouls, N.: GeneSyst: A Tool to Reason About Behavioral Aspects of B Event Specifications, Application to Security Properties. In: Treharne, H., King, S., C. Henson, M., Schneider, S. (eds.) ZB 2005. LNCS, vol. 3455, pp. 299–318. Springer, Heidelberg (2005)CrossRefGoogle Scholar
  9. 9.
    Back, R.J.R., Kurki-Suonio, R.: Decentralization of Process Nets with Centralized Control. In: The 2nd Symposium on Principles on Distributed Computing, pp. 131–142 (1983)Google Scholar
  10. 10.
    SICS, SICStus Prolog (2006), website:
  11. 11.
    Plosila, J., Sere, K.: Action Systems in Pipelined Processor Design. In: 3rd International Symposium on Advanced Research in Asynchronous Circuits and Systems (ASYNC 1997), p. 156 (1997)Google Scholar
  12. 12.
    Hemani, A., Jantch, A., Kumar, K., Postula, A., Öberg, J., Millberg, M., Lindqvist, D.: Network on a Chip: An architecture for billion transistor era. In: IEEE NorChip Conference (2000)Google Scholar
  13. 13.
    Marculescu, R., Ogras, U., Peh, L.-S., Enright Jerger, N., Hoskote, Y.: Outstanding Research Problems in NoC Design: System, Microarchitecture, and Circuit Perspectives. IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems 28(1), 3–21 (2009)CrossRefGoogle Scholar
  14. 14.
    Hu, J., Marculescu, R.: Energy-aware mapping for tile-based NOC architectures under performance constraints. In: Asia South Pacific Design Automation Conference, Japan, pp. 233–239 (2003)Google Scholar
  15. 15.
    Childs, A., Greenwald, J., Ranganath, V.P., Deng, X., Dwyer, M.B., Hatcliff, J., Jung, G., Shanti, P., Singh, G.: Cadena: An Integrated Development Environment for Analysis, Synthesis, and Verification of Component-Based Systems. In: Wermelinger, M., Margaria-Steffen, T. (eds.) FASE 2004. LNCS, vol. 2984, pp. 160–164. Springer, Heidelberg (2004)CrossRefGoogle Scholar
  16. 16.
    Yang, Y.S., Bahn, J.H., Lee, S.E., Bagherzadeh, N.: Parallel and Pipeline Processing for Block Cipher Algorithms on a Network-on-Chip. In: Sixth International Conference on Information Technology: New Generations, pp. 849–854 (2009)Google Scholar
  17. 17.
    Branca, M., Camerini, L., Ferrandi, F., Lanzi, P.L., Pilato, C., Sciuto, D., Tumeo, A.: Evolutionary Algorithms for the Mapping of Pipelined Applications onto heterogeneous Embedded Systems. In: 11th Annual Conference on Genetic and Evolutionary Computation, GECCO 2009 (2009)Google Scholar
  18. 18.
    Zheng, J., Wu, D., Xie, D., Gao, W.: A novel pipeline design for H.264 CABAC decoding. In: Ip, H.H.-S., Au, O.C., Leung, H., Sun, M.-T., Ma, W.-Y., Hu, S.-M. (eds.) PCM 2007. LNCS, vol. 4810, pp. 559–568. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  19. 19.
    McEwan, A.A., Schneider, S.: Modeling and analysis of the AMBA bus using CSP and B. In: Communicating Process Architectures, pp. 379–398 (2007)Google Scholar
  20. 20.
    Petre, L., Sere, K., Tsiopoulos, L., Liljeberg, P., Plosila, J.: Towards Self-Placing Applications on 2D- and 3D-NoCs. In: Cong-Vinh, P. (ed.) Autonomic Networking-on-Chip: Bio-inspired Specification, Development, and Verification, Embedded Multi-core System(EMS) Book Series. CRC Press, Boca Raton (to appear, 2011)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Luigia Petre
    • 1
  • Kaisa Sere
    • 1
  • Leonidas Tsiopoulos
    • 1
  1. 1.Department of Information TechnologiesÅbo Akademi UniversityTurkuFinland

Personalised recommendations