B to CSP Migration: Towards a Formal and Automated Model-Driven Engineering of Hardware/Software Co-design

  • Marcel Vinicius Medeiros Oliveira
  • David B. P. Déharbe
  • Luís C. D. S. Cruz
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7021)


This paper presents a migration approach from a class of hierarchical B models to CSP. The B models follow a so-called polling pattern, suitable for reactive systems, and are automatically translated into a set of communicating CSP processes with the same behaviour. The structure of the CSP model matches that of the B model and may be formally analysed using model checking. Selected CSP processes may then be further refined and synthesised to hardware, while the remaining modules would be mapped to software using B refinements. The translation proposed here paves the way for a model-based approach to hardware and software co-design employing complementary formal methods.


Model-driven engineering co-design CSP 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Abrial, J.-R.: The B-book: Assigning Programs to Meanings. Cambridge University Press, Cambridge (1996)CrossRefzbMATHGoogle Scholar
  2. 2.
    Butler, M.J.: An approach to the design of distributed systems with B AMN. In: Till, D., Bowen, J., Hinchey, M.G. (eds.) ZUM 1997. LNCS, vol. 1212, pp. 223–241. Springer, Heidelberg (1997)Google Scholar
  3. 3.
    Butler, M.J.: csp2B: a practical approach to combining CSP and B. FACJ 12(3), 182–198 (2000)zbMATHGoogle Scholar
  4. 4.
    Déharbe, D., Moreira, A.M., Muniz Silva, P., Russo Jr., A.: Modelling control systems in b: an industrial case study. In: SBMF 2007, pp. 112–127 (2007)Google Scholar
  5. 5.
    Evans, N., Treharne, H.: Linking Semantic Models to Support CSP||B Consistency Checking. Electr. Notes Theor. Comput. Sci. 145, 201–217 (2006)CrossRefzbMATHGoogle Scholar
  6. 6.
    Fischer, C.: CSP-OZ: A combination of Object-Z and CSP. In: FMOODS, vol. 2, pp. 423–438. Chapman & Hall, Boca Raton (1997)Google Scholar
  7. 7.
    Formal Systems Ltd. FDR: User Manual and Tutorial, version 2.82 (2005)Google Scholar
  8. 8.
    Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)Google Scholar
  9. 9.
    Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice-Hall (1998)Google Scholar
  10. 10.
    Mens, T., Van Gorp, P.: A taxonomy of model transformation. ENTCS 152, 125–142 (2006)Google Scholar
  11. 11.
    Milner, R.: Communication and Concurrency. Prentice-Hall (1989)Google Scholar
  12. 12.
    Oliveira, M.V.M., Cavalcanti, A.L.C., Woodcock, J.C.P.: A UTP Semantics for Circus. FACJ (2008)Google Scholar
  13. 13.
    Oliveira, M.V.M., Woodcock, J.C.P.: Automatic Generation of Verified Concurrent Hardware. In: Butler, M., Hinchey, M.G., Larrondo-Petrie, M.M. (eds.) ICFEM 2007. LNCS, vol. 4789, pp. 286–306. Springer, Heidelberg (2007)CrossRefGoogle Scholar
  14. 14.
    Roscoe, A.W., Woodcock, J.C.P., Wulf, L.: Non-interference through Determinism. In: Gollmann, D. (ed.) ESORICS 1994. LNCS, vol. 875, pp. 33–54. Springer, Heidelberg (1994)Google Scholar
  15. 15.
    Schneider, S., Treharne, H., McEwan, A., Ifill, W.: Experiments in Translating CSP||B to Handel-C. In: CPA - Communicating Process Architectures Conference. Concurrent Systems Engineering Series, vol. 66, pp. 115–133. IOS Press (2008)Google Scholar
  16. 16.
    Taguchi, K., Araki, K.: The state-based CCS semantics for concurrent Z specification. In: ICFEM, pp. 283–292. IEEE (1997)Google Scholar
  17. 17.
    Woodcock, J.C.P., Davies, J.: Using Z—Specification, Refinement, and Proof. Prentice-Hall, Englewood Cliffs (1996)zbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2011

Authors and Affiliations

  • Marcel Vinicius Medeiros Oliveira
    • 1
  • David B. P. Déharbe
    • 1
  • Luís C. D. S. Cruz
    • 1
  1. 1.Universidade Federal do Rio Grande do NorteBrazil

Personalised recommendations