Efficient re-resolution of SMT specifications for evolving software architectures

TY - GEN

T1 - Efficient re-resolution of SMT specifications for evolving software architectures

AU - Johnson, Kenneth

AU - Calinescu, Radu

PY - 2014/1/1

Y1 - 2014/1/1

N2 - 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.

AB - 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.

KW - Domain-Specific Languages

KW - Incremental Re-resolution

KW - Sat-isfiability Modulo Theory

UR - http://www.scopus.com/inward/record.url?scp=84904466305&partnerID=8YFLogxK

U2 - 10.1145/2602576.2602578

DO - 10.1145/2602576.2602578

M3 - Conference contribution

AN - SCOPUS:84904466305

SN - 9781450325769

SP - 93

EP - 102

BT - QoSA 2014

PB - ACM

T2 - 10th International ACM SIGSOFT Conference on Quality of Software Architectures, QoSA 2014

Y2 - 30 June 2014 through 4 July 2014

ER -