Practical application of formal methods for specification and analysis of software architecture

With the ever-growing pace of technological advancement, computer software is required to become increasingly complex to meet the demands of today's leading edge technologies, and their applications. However fulfilling this requirement creates new, previously unknown, problems pertaining to non-functional properties of software. Specifically, as the software complexity escalates, it becomes increasingly difficult to scale the software in order to cope with the sometimes overwhelming demand created by system growth. It is therefore essential to have processes for addressing the issues associated with scalability that arise due to the complexity in software systems. In this paper we describe an approach aimed at fulfilling the need for such processes. A combination of Object-Z and temporal logic is used to create an architectural description open to further analysis. We also demonstrate the practicality of this methodology within the context of the Coordinated Adaptive Traffic System (CATS).