Formal modeling and automated verification of design patterns

Design patterns capture expert design experience in generic design structure and behavior. To reuse design experience, a design pattern needs to be instantiated from its generic template to the application design in a particular context. It can be integrated with other patterns to solve multiple design problems. The instantiation and integration of design patterns are two important processes when a designer reuses design experience in an application. It is important to know whether the instantiation and integration commute because it can save considerable time and effort of software designers for trial-and-error. In this thesis, we investigate the commutability of the instantiation and integration of design patterns. We provide rigorous proofs on the conditions when the order of these two design processes does not matter. Our results allow the software designers to choose the design processes with assurance of their equivalence. The benefits of our work include helping the designers to make informed design decisions based on the convergence of different design processes and reducing the possible design choices, and thus the complexity of software development. Software security becomes critically important when various malicious attacks that explore the security holes in software systems. To avoid security problems, a large software system design may apply many security patterns to reuse good security solutions. Security patterns document expert solutions to common security problems and capture best practices on secure software design and development. Although each security pattern describes a good design guideline, the compositions of these security patterns may not be consistent and encounter problems and flaws. Therefore, the compositions of security patterns may not be even secure. In this thesis, we developed methods to transform design patterns and their integration into formal specification. In addition, we proved the correctness of the transformation. This approach allows us to automatically verify security pattern compostions and discover composition errors and problems early in the design stage.