SAwUML - UML-based, contractual software architectures and their formal analysis using SPIN

Abstract

UML is without doubt the top preferred software modelling language by practitioners. However, UML remains inadequate for the software architecture level of design due to its weak support for some important requirements including multiple viewpoints, connectors, and formal analysis. In this paper, the SAwUML architecture description language is proposed to improve UML for the high-level, precise specifications of the structural and behavioural design decisions and their formal analysis. To this end, SAwUML combines UML's component and sequence diagrams together under the same notation set. Using the component diagram, practitioners can specify their system components that are connected via the required and provided ports and interact over the port method-calls. Whenever a component port is clicked, a UML sequence diagram can be drawn for specifying the port methods in terms of the request and response messages that are exchanged between the interacting components. SAwUML extends the formal Design-by-Contract approach for the behaviour specifications of the port methods drawn in the sequence diagram. SAwUML's contract extension considers both the request and response messages of method-calls, deciding on when method-calls can be requested/received, the method parameters/results to be assigned, and how the component post-state should be after method-calls. SAwUML is supported with a modelling tool for specifying the structural and behavioural design decisions together and any system-level properties in the linear temporal logic. The tool can automatically translate the software architectures in SAwUML into a formal ProMeLa model. Then the SPIN model checker can be used to verify the resulting ProMeLa models for the pre-defined properties - i.e., deadlock and incompleteness- and any user-defined properties. (C) 2018 Elsevier Ltd. All rights reserved.