Advertisement

BTS: A Tool for Formal Component-Based Development

  • Dalay Israel de Almeida PereiraEmail author
  • Marcel Vinicius Medeiros Oliveira
  • Madiel S. Conserva Filho
  • Sarah Raquel Da Rocha Silva
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10510)

Abstract

In previous work we have presented a CSP based approach for developing component-based asynchronous systems, \(\mathcal {B}\mathcal {R}\mathcal {I}\mathcal {C}\), which guarantees deadlock freedom by construction. It uses CSP to specify the constraints and interactions between the components to allow a formal verification of the composition’s behaviour. Following this work, we also proposed an efficient approach for ensuring livelock analysis by construction. In this work we present a tool that automates the verification of component composition by automatically generating and checking the side conditions imposed by both approaches. The tool also includes a support to \(\mathcal {B}\mathcal {R}\mathcal {I}\mathcal {C}\mathcal {K}\), an optimisation of \(\mathcal {B}\mathcal {R}\mathcal {I}\mathcal {C}\), that enriches the components with metadata containing additional useful information, which considerably reduces the costs of the composition verifications.

Keywords

Component-based systems CSP Compositional analysis Deadlock verification Livelock verification 

References

  1. 1.
    Åkerholm, M., Carlson, J., Fredriksson, J., Hansson, H., Håkansson, J., Möller, A., Pettersson, P., Tivoli, M.: The save approach to component-based development of vehicular systems. J. Syst. Softw. 80(5), 655–667 (2007)CrossRefGoogle Scholar
  2. 2.
    Antonino, P.R.G., Oliveira, M.M., Sampaio, A.C.A., Kristensen, K.E., Bryans, J.W.: Leadership election: an industrial sos application of compositional deadlock verification. In: Badger, J.M., Rozier, K.Y. (eds.) NFM 2014. LNCS, vol. 8430, pp. 31–45. Springer, Cham (2014). doi: 10.1007/978-3-319-06200-6_3 CrossRefGoogle Scholar
  3. 3.
    Arbab, F.: Reo: a channel-based coordination model for component composition. Mathematical Struct. Comput. Sci. 14(03), 329–366 (2004)MathSciNetCrossRefzbMATHGoogle Scholar
  4. 4.
    Barrett, C., Conway, C.L., Deters, M., Hadarean, L., Jovanović, D., King, T., Reynolds, A., Tinelli, C.: CVC4. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 171–177. Springer, Heidelberg (2011). doi: 10.1007/978-3-642-22110-1_14 CrossRefGoogle Scholar
  5. 5.
    Barrett, C., Stump, A., Tinelli, C.: The smt-lib standard: Version 2.0 (2010). www.SMT-LIB.org
  6. 6.
    Beneš, N., Brim, L., Černá, I., Sochor, J., Vařeková, P., Zimmerová, B., et al.: The coin tool: modelling and verification of interactions in component-based systems. Electronic Notes in Theoretical Computer Science, pp. 221–225 (2008)Google Scholar
  7. 7.
    Bouton, T., Caminha B. de Oliveira, D., Déharbe, D., Fontaine, P.: veriT: an open, trustable and efficient SMT-solver. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 151–156. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-02959-2_12 CrossRefGoogle Scholar
  8. 8.
    Brim, L., Černá, I., Vařeková, P., Zimmerova, B.: Component-interaction automata as a verification-oriented component-based system specification. ACM SIGSOFT Softw. Eng. Not. 31, 4 (2005)CrossRefGoogle Scholar
  9. 9.
    Bruin, H.: A grey-box approach to component composition. In: Czarnecki, K., Eisenecker, U.W. (eds.) GCSE 1999. LNCS, vol. 1799, pp. 195–209. Springer, Heidelberg (2000). doi: 10.1007/3-540-40048-6_15 CrossRefGoogle Scholar
  10. 10.
    Butler, M., Hallerstede, S.: The rodin formal modelling tool. In: BCS-FACS Christmas 2007 Meeting-Formal Methods In Industry, London (2007)Google Scholar
  11. 11.
    Filho, M.S.C., Oliveira, M.V.M., Sampaio, A., Cavalcanti, A.: Local livelock analysis of component-based models. In: Ogata, K., Lawford, M., Liu, S. (eds.) ICFEM 2016. LNCS, vol. 10009, pp. 279–295. Springer, Cham (2016). doi: 10.1007/978-3-319-47846-3_18 CrossRefGoogle Scholar
  12. 12.
    Object Management Group. The Common Object Request Broker (CORBA): Architecture and Specification. Object Management Group (1995)Google Scholar
  13. 13.
    Gurgel, A.C., Castro, C.G., Oliveira, M.V.M.: Tool support for the circus refinement calculus. ABZ 8, 349–349 (2008)Google Scholar
  14. 14.
    Hoare, C.A.R.: Communicating sequential processes. Commun. ACM 21(8), 666–677 (1978)CrossRefzbMATHGoogle Scholar
  15. 15.
    McIlroy, M.D., Buxton, J.M., Naur, P., Randell, B.: Mass-produced software components. In: Proceedings of the 1st International Conference on Software Engineering, Garmisch Pattenkirchen, Germany. sn (1968)Google Scholar
  16. 16.
    Moura, L., Bjørner, N.: Z3: an efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008). doi: 10.1007/978-3-540-78800-3_24 CrossRefGoogle Scholar
  17. 17.
    Oliveira, M.V.M., Antonino, P.R.G., Ramos, R.T., Sampaio, A.C.A., Mota, A.C., Roscoe, A.W.: Rigorous development of component-based systems using component metadata and patterns. Formal Aspects Comput., 1–68 (2016)Google Scholar
  18. 18.
    Oliveira, M.V.M., Sampaio, A.C.A., Antonino, P.R.G., Oliveira, J.D., Filho, M.C., Bryans, J.: Compositional analysis and design of CML models. Technical Report D24.4, COMPASS Deliverable (2014)Google Scholar
  19. 19.
    Oliveira, M.V.M., Sampaio, A.C.A., Antonino, P.R.G., Ramos, R.T., Cavancalti, A.L.C., Woodcock, J.C.P.: Compositional Analysis and Design of CML Models. Technical Report D24.1, COMPASS Deliverable (2013)Google Scholar
  20. 20.
    Ramos, R., Sampaio, A., Mota, A.: Systematic development of trustworthy component systems. In: Cavalcanti, A., Dams, D.R. (eds.) FM 2009. LNCS, vol. 5850, pp. 140–156. Springer, Heidelberg (2009). doi: 10.1007/978-3-642-05089-3_10 CrossRefGoogle Scholar
  21. 21.
    Gibson-Robinson, T., Armstrong, P., Boulgakov, A., Roscoe, A.W.: FDR3 — a modern refinement checker for CSP. In: Ábrahám, E., Havelund, K. (eds.) TACAS 2014. LNCS, vol. 8413, pp. 187–201. Springer, Heidelberg (2014). doi: 10.1007/978-3-642-54862-8_13 CrossRefGoogle Scholar
  22. 22.
    Roscoe, A.W., Hoare, C.A.R., Bird, R.: The Theory and Practice of Concurrency, vol. 1. Prentice Hall, Englewood Cliffs (1998)Google Scholar
  23. 23.
    Sentilles, S., Pettersson, A., Nystrom, D., Nolte, T., Pettersson, P., Crnkovic, I.: Save-ide-a tool for design, analysis and implementation of component-based embedded systems. In: Proceedings of the 31st International Conference on Software Engineering, pp. 607–610. IEEE Computer Society (2009)Google Scholar
  24. 24.
    Silva, S.R.R.: Bts: uma ferramenta de suporte ao desenvolvimento sistemático de sistemas confiáveis baseados em componentes. Master’s thesis, Universidade Federal do Rio Grande do Norte (2013)Google Scholar
  25. 25.
    Sy, O., Bastide, R., Palanque, P., Le, D., Navarre, D.: Petshop: a case tool for the petri net based specification and prototyping of corba systems. In: Petri Nets 2000, p. 78 (2000)Google Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  • Dalay Israel de Almeida Pereira
    • 1
    Email author
  • Marcel Vinicius Medeiros Oliveira
    • 1
  • Madiel S. Conserva Filho
    • 1
  • Sarah Raquel Da Rocha Silva
    • 1
  1. 1.Universidade Federal do Rio Grande do NorteNatalBrazil

Personalised recommendations