Abstract
Designing the software architecture of a system is an important step in creating a system that will meet both the functional and non-functional requirements. Bass, Clements and Kazman in "Software Architecture in Practice" propose a method to use design tactics to create the Software Architecture of a system. For each quality attribute a set of design tactics were developed. Security is one such quality attribute. The security requirements of a system must be taken into account from the start. Adding security adversely affects, the other quality attributes so it is difficult to add security to a product after it has been designed. When defining the security tactics of a system, there is currently no way to formally prove the implementation of the tactics. There is a semantic gap between the software architecture, high level design and implementation of a system. One way to bridge this gap is to use formal specifications. The formal specifications can be used as a template when designing new systems and to analyze the architecture more rigorously. This project provides a Z specification for the Software Architectural Tactics for the Security Quality Attribute. A model of a system is created and each tactic is defined with respect to the model. Each tactic is independent however, the system encompasses all the required functionality for all the tactics.