Efficient re-resolution of SMT specifications for evolving software architectures

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

We present a generic method for the effcient constraint re- resolution of a component-based software architecture after changes such as addition, removal and modification of components. Given a formal description of an evolving system as a constraint-specification problem, our method identifies and executes the re-resolution steps required to verify the system's compliance with constraints after each change. At each step, satisfiability modulo theory (SMT) techniques determine the satisfiability of component constraints expressed as logical formulae over suitably chosen theories of arithmetic, reusing results obtained in previous steps. We illustrate the application of the approach on a constraint- satisfaction problem arising from cloud-deployed software services. The incremental method is shown to re-resolve sys- tem constraints in a fraction of the time taken by standard SMT resolution.

Original languageEnglish
Title of host publicationQoSA 2014
Subtitle of host publicationProceedings of the 10th International ACM SIGSOFT Conference on Quality of Software Architectures (Part of CompArch 2014)
PublisherACM
Pages93-102
Number of pages10
ISBN (Print)9781450325769
DOIs
Publication statusPublished - 1 Jan 2014
Event10th International ACM SIGSOFT Conference on Quality of Software Architectures, QoSA 2014 - Marcq-en-Baroeul, United Kingdom
Duration: 30 Jun 20144 Jul 2014

Conference

Conference10th International ACM SIGSOFT Conference on Quality of Software Architectures, QoSA 2014
Country/TerritoryUnited Kingdom
CityMarcq-en-Baroeul
Period30/06/144/07/14

Keywords

  • Domain-Specific Languages
  • Incremental Re-resolution
  • Sat-isfiability Modulo Theory

Cite this