Skip to main content
SpringerLink
Log in
Book cover

Brazilian Symposium on Formal Methods

SBMF 2021: Formal Methods: Foundations and Applications pp 1–16Cite as

A Two-Level Approach Based on Model Checking to Support Architecture Conformance Checking

  • Conference paper
  • First Online:

  • 194 Accesses

Part of the book series: Lecture Notes in Computer Science ((LNPSE,volume 13130))

Abstract

We propose a Model Checking based method to aid Architecture Conformance Checking, which is a fundamental analysis to ensure software quality, dependability and maintainability. In this work, a new logic, which combines temporal logic, hybrid logic and a new logical operator in order to formalize software specifications, is proposed. The method described in this paper uses two structures, namely call graphs and software version graphs. The first one is used to check specifications related to classes and methods and we apply it intending to analyze a specific software version. The latter one gives us an overview of the software development process and we employ it to check global software requirements. These two graphs allow us to design a two-level checking method. The first level deals with specifications of a single software version that must be inspected in the call graph. The second level handles the global requirements throughout all software versions. Using our new operator and a function, we are able to use the same logic in both levels, allowing them to communicate with each other and handle the verification process in a neat and uniform manner. Our two-level approach is the great differential of this work, since the current approaches available in the literature focus on an unique software version at a time. We also present the general idea of an algorithm, which has polynomial time complexity, to perform Model Checking for our proposed temporal logic.

This research was supported by the Brazilian National Council for Scientific and Technological Development (CNPq) under the grant number 424188/2016-3.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   44.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   59.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  1. Cqlinq syntax. https://www.ndepend.com/docs/cqlinq-syntax/#architect. Accessed 4 Aug 2021

  2. Lattix architect. https://www.lattix.com/products-architecture-issues/#architect. Accessed 4 Aug 2021

  3. Sonargraph-architect (2017)

    Google Scholar 

  4. Aldrich, J., Chambers, C., Notkin, D.: ArchJava: connecting software architecture to implementation. In: Proceedings of the 24th International Conference on Software Engineering, ICSE 2002, pp. 187–197. IEEE (2002)

    Google Scholar 

  5. Baier, C., Katoen, J.P.: Principles of Model Checking. The MIT Press, New York (2008)

    MATH  Google Scholar 

  6. Beyersdorff, O., Meier, A., Thomas, M., Vollmer, H., Mundhenk, M., Schneider, T.: Model checking CTL is almost always inherently sequential. In: 2009 16th International Symposium on Temporal Representation and Reasoning (2009)

    Google Scholar 

  7. Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press (2002). https://books.google.com.br/books?id=gFEidNVDWVoC

  8. Chacon, S., Straub, B.: Pro Git, 2nd edn. Apress, New York (2014)

    Book  Google Scholar 

  9. Czepa, C., Tran, H., Zdun, U., Thi Kim, T.T., Weiss, E., Ruhsam, C.: On the understandability of semantic constraints for behavioral software architecture compliance: a controlled experiment. In: 2017 IEEE International Conference on Software Architecture (ICSA), pp. 155–164 (2017)

    Google Scholar 

  10. Deitel, P., Deitel, H.: Java How to Program - Early Objects, 10th edn. Prentice Hall Press, Englewood Cliffs (2014)

    MATH  Google Scholar 

  11. Duszynski, S., Knodel, J., Lindvall, M.: SAVE: software architecture visualization and evaluation. In: 2009 13th European Conference on Software Maintenance and Reengineering, pp. 323–324. IEEE (2009)

    Google Scholar 

  12. Fisher, M.: An Introduction to Practical Formal Methods Using Temporal Logic, 1st edn. Wiley Publishing, Chichester (2011)

    Book  Google Scholar 

  13. Grove, D., Chambers, C.: A framework for call graph construction algorithms. ACM Trans. Program. Lang. Syst. (TOPLAS) 23(6), 685–746 (2001)

    Article  Google Scholar 

  14. Herold, S.: Architectural compliance in component-based systems. Ph.D. thesis, Clausthal University of Technology (2011)

    Google Scholar 

  15. Hoffmann, A.B.G., et al.: Um modelo para o controle de versões de sistemas para apoio ao desenvolvimento colaborativo através da web (2002)

    Google Scholar 

  16. Hou, D., Hoover, H.J.: Using SCL to specify and check design intent in source code. IEEE Trans. Software Eng. 32(6), 404–423 (2006)

    Article  Google Scholar 

  17. Iadarola, G., Martinelli, F., Mercaldo, F., Santone, A.: Call graph and model checking for fine-grained android malicious behaviour detection. Appl. Sci. 10(22), 7975 (2020)

    Article  Google Scholar 

  18. de Lima Meneses Filho, J.: Uma Solução para Verificação Estática de Conformidade Arquitetural do Tratamento de Exceção. Master’s thesis, Universidade Federal do Ceará (2016)

    Google Scholar 

  19. Mitschke, R., Eichberg, M., Mezini, M., Garcia, A., Macia, I.: Modular specification and checking of structural dependencies. In: Proceedings of the 12th Annual International Conference on Aspect-Oriented Software Development, pp. 85–96 (2013)

    Google Scholar 

  20. Passos, L., Terra, R., Valente, M.T., Diniz, R., Mendonça, N.: Static architecture-conformance checking: an illustrative overview. IEEE Softw. 27(5), 82–89 (2010). https://doi.org/10.1109/MS.2009.117

    Article  Google Scholar 

  21. Perry, D.E., Wolf, A.L.: Foundations for the study of software architecture. SIGSOFT Softw. Eng. Notes 17(4), 40–52 (1992)

    Article  Google Scholar 

  22. Preston-Werner, T.: Semantic versioning 2.0.0. https://semver.org/spec/v2.0.0.html. Accessed 4 Aug 2021

  23. Ryan, M., Huth, M.: Logic in Computer Science: Modelling and Reasoning about Systems. Cambridge University Press, New York (2004)

    MATH  Google Scholar 

  24. Schröder, S.: Ontology-based architecture enforcement: defining and enforcing software architecture as a concept language using ontologies and a controlled natural language. Ph.D. thesis, Staats-und Universitätsbibliothek Hamburg Carl von Ossietzky (2020)

    Google Scholar 

  25. de Silva, L., Balasubramaniam, D.: Controlling software architecture erosion: a survey. J. Syst. Softw. 85(1), 132–151 (2012)

    Article  Google Scholar 

  26. Sommerville, I.: Software Engineering, 9th edn. Addison-Wesley Publishing Company, Boston (2010)

    MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Universidade Federal do Ceará, Fortaleza, Brazil

    Bruno Menezes & Ana Teresa Martins

  2. Instituto Federal de Educação, Ciência e Tecnologia do Ceará IFCE, Maracanaú, Brazil

    Thiago Alves Rocha

Authors
  1. Bruno Menezes
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Ana Teresa Martins
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Thiago Alves Rocha
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Bruno Menezes .

Editor information

Editors and Affiliations

  1. Departamento de Ciência da Computação, Universidade Federal de Minas Gerais, Belo Horizonte, Minas Gerais, Brazil

    Sérgio Campos

  2. College of Information and Computer Sciences, University of Massachusetts, Amherst, MA, USA

    Marius Minea

Rights and permissions

Reprints and permissions

Copyright information

© 2021 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Menezes, B., Martins, A.T., Rocha, T.A. (2021). A Two-Level Approach Based on Model Checking to Support Architecture Conformance Checking. In: Campos, S., Minea, M. (eds) Formal Methods: Foundations and Applications. SBMF 2021. Lecture Notes in Computer Science(), vol 13130. Springer, Cham. https://doi.org/10.1007/978-3-030-92137-8_1

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-92137-8_1

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-92136-1

  • Online ISBN: 978-3-030-92137-8

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation