PhD thesis: Static and Dynamic Verification of Indirect Data Sharing in Component-based Application
Abstract
Modern software systems evolve towards modularly composed applications, in which existing software components are reused in new software compositions. Current component-based software systems often promote simple syntactical interfaces to make the wiring of components simple. In practice however, these loosely-coupled components sometimes tend to have semantical dependencies, for example by passing data to each other on a shared data repository as is the case in data-centered applications. Typically, these hidden semantical dependencies are not checked at compile-time and lead to run-time errors in current software systems.
The main contribution of this thesis is an approach to reduce the number of run-time errors due to broken data dependencies in data-centered component-based applications. We have built up extensive hands-on experience with such applications in two application domains: networking software and web applications. This experience shows that errors caused by broken data dependencies are important in practice. Our approach is based on the formal verification of a composition property, the no broken data dependencies property. This formal verification is achieved in two steps.
In a first step, we statically verify the desired composition property in deterministic software compositions. To do so, each component of the composition is extended with a component contract, stating in a problem-specific contract language what the shared data interactions of the component are. These contracts are then verified in two steps. First, the compliance of the component's implementation with its contract is checked. Next, the composition property is verified within the given composition relying on the different component contracts. In a second step, we extend the verification of the desired composition property towards reactive software systems by combining the static verification approach with run-time checking. In addition to the approach for deterministic compositions, the expected, reactive protocol between the client and the server is expressed in a labelled state machine. Next, we statically verify with the earlier proposed solution whether or not the desired property is violated in a given composition, while assuming that the actual interaction protocol complies with the expressed state machine. Finally, we use the run-time checking capabilities of a Web Application Firewall to guarantee that the incoming requests of a user's session comply to the verified labelled state machine and thus that the no broken data dependencies composition property also holds in the given composition.
Finally, we validated the formal verification of the no broken data dependencies composition property in both a deterministic and a reactive software composition. The static verification approach is successfully applied to the medium-sized open-source webmail application GatorMail, in which more than 1350 shared data interactions are present. In addition, the combination of static verification and run-time checking by means of a Web Application Firewall is validated in the Duke's BookStore application, a reactive e-commerce application. In both case studies, a limited annotation and verification overhead was measured, and they both illustrated that the presented solution is scalable to larger, real-life software applications thanks to the modular specification and verification process.
Download
Text of the dissertation: PhD-Desmet.pdf
Presentation PhD defense: PhD-Desmet-Lieven.ppt
Promotors:
- Prof. Dr. ir. Frank Piessens
- Prof. Dr. ir. Pierre Verbaeten
Jury:
- Prof. Dr. ir. W. Sansen, chair of the jury
- Prof. Dr. ir. F. Piessens, promotor
- Prof. Dr. ir. P. Verbaeten, promotor
- Prof. Dr. ir. E. Steegmans
- Prof. Dr. ir. W. Joosen
- Prof. Dr. T. Holvoet
- Prof. Dr. D. Gurov (KTH Royal Institute of Technology)
