Home // SOFTENG 2016, The Second International Conference on Advances and Trends in Software Engineering // View article

Verification of Architectural Constraints on Interaction Protocols Among Modules

Authors:
Stuart Siroky
Rodion Podorozhny
Guowei Yang

Keywords: verification; architecture; symbolic execution; call graph.

Abstract:
The importance of adhering to an adopted architectural style throughout software development and maintenance has been long recognized. This paper introduces an approach to efficiently checking the correspondence of architectural constraints on sequences of method invocations, i.e., interaction protocols involving more than two modules. Our approach combines parameterized slicing and non-deterministic symbolic execution. Slicing produces an executable portion of the bytecode of the system under analysis relevant to the given architectural property, and symbolic execution is applied to the slice to check all paths and all interleavings for any violations of the given architectural constraints. We have implemented our approach in a prototype, where IBM WALA library is used for slicing, Javassist is used to aid in the mocking of the unused code, and Symbolic PathFinder is used for symbolic execution. Two case studies on verification of Model-View-Controller systems have demonstrated the usefulness of our approach. In particular, property guided automatic slicing, in some cases, significantly reduces the size of the input to the symbolic execution, resulting in a reduction of verification time.

Pages: 140 to 145

Copyright: Copyright (c) IARIA, 2016

Publication date: February 21, 2016

Published in: conference

ISSN: 2519-8394

ISBN: 978-1-61208-458-9

Location: Lisbon, Portugal

Dates: from February 21, 2016 to February 25, 2016