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

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.