SAWUML - UML-based, Contractual Software Architecture Modelling Language
SA-UML has been offered as a new software modelling language that is based on UML and Design-by-Contract. Designers can specify their software architectures using UML's component diagram in terms of components that interact with each other via their provided and required ports. Designers can specify the port behaviours via UML's sequence diagram which is extended with contracts. Each port is specified in terms of the methods that are provided/required via that port and for each method, its behaviour is specified as a contract.
Below is the notation set for SA-UML, which consists of the symbols for components and the provided & required types of ports.
Whenever designers click on the components, a new dialog box opens (as depicted in the left-most column of the below table) for specifying component details, i.e., the component type name, component parameters, and the component state data variables. Note that component state data are updated by the port methods of that component, which are either requested via the ports (required port) or offered outside (provided port). Designers can specify the port methods using an extended form of UML's sequence diagram with the Design-by-Contract approach. Whenever the port symbols in a component diagram is clicked, a new (sub) editor opens for drawing the sequence diagrams. In the sequence diagrams (see the below table), designers can specify each method in terms of its request and response messages and attach each message a SA-UML contract that describes its behaviour.
Tool Support
SA-UML is supported with a toolset that includes a modelling editor and a translator. Using the modelling editor, designers can specify their UML-based, contractual software architectures and then use the translator (i.e., embedded within the modelling editor) for translating the SA-UML specifications in SPIN's ProMeLa input language for formal verification. The resulting ProMeLa models can be exhaustively analysed using the SPIN model checker for deadlock and incomplete behaviour specifications. Moreover, SA-UML also supports via its modelling editor the specifications of system-level properties in the form of linear temporal logic (LTL). The SPIN model checker can then formally verify the system specifications for these LTL properties (SPIN accepts LTL).
SA-UML's modelling editor (and its translator) has been developed using the Metaedit+ language development framework. So, you need to install the Metaedit+ application first and then download SA-UML's project folder that needs to be put inside the Metaedit+ folder created in your local machine. Then, you should be able to use SA-UML's modelling editor and translator, which is depicted below.
Please click here to download SA-UML's toolset.
Click for Version 2 with some new improvements. These improvements include the modularisation of the generated ProMeLa code with macro definitions and the better visualisation of the behaviour view specifications in the sequence diagram.
Case Studies
SA-UML has been illustrated via three well-known case studies that are given below. The SA-UML specifications of the case-studies can be accessed from the Metaedit+ modelling environment that can be downloaded here . Note that the modelling editor is capable of saving/editing the SA-UML specifications.
Gas Station*
We consider here the classic architectural case study of a gas station [*] for a number of customers N, which in our case is equal to two. As the figure shows, the gas station has one cashier component with N event consumer ports through which it receives payment events and N event emitter ports through which it sends events to release a respective pump. The system has a pump component that also has one event consumer port to receive release pump events and N method provided ports through which it receives requests for gas.Finally the system has N components of type customer, each of which has two ports. One is an event emitter port that sends payment events and the other is a method required port that calls the pump method.
* Naumovich G, Avrunin GS, Clarke LA, Osterweil LJ. Applying static analysis to software architectures. ESEC/ SIGSOFT FSE, Lecture Notes in Computer Science, vol. 1301, Jazayeri M, Schauer H (eds.), Springer, 1997; 77–93.
The translated ProMeLa code from the SA-UML specification of gas station:
Lunar Lander**
Lunar lander is essentially a lander part of a spacecraft that enables the spacecraft to land on the surface of the moon safely. It has first been considered by Taylor etal. [**] as a case study for specifying software architectures. Later on, Maoz etal. has specified it using their own language MontiArc [Maoz et al.(2013)]. The structure of the lunar lander is described as an interaction of three components, DataStore, Calculation, and UserInter f ace. While the DataStore stores the data of the lunar lander (e.g., its height, velocity, fuel, and etc.), the Calculation receives and updates them based on the burn- rate input of the UserInterface, and stores them back in the DataStore.
** Richard N. Taylor, Nenad Medvidovic, and Eric M. Dashofy. Software Architecture - Foundations, Theory, and Practice. Wiley, 2010. ISBN 978-0-470-16774-8.
The translated ProMeLa code from the SAw-UML specification of lunar lander:
AEGIS Combat System
The AEGIS system has been developed for navy ships to make them capable of controlling their weapons against enemies. The AEGIS system has firstly been tackled by Wright [Allen and Garlan, 1996]. Therein, a formal specification of the AEGIS is given in Wright [Allen and Garlan, 1997], and also the evaluation of its analysis. As depicted in the figure, AEGIS could informally be specified as a set of components interacting with each other. The Experiment Control, at the top of the diagram, essentially provides linked components the information obtained via sensors.The track information is, for instance, required by the Track Server which stores it and provides other components (Doctrine Validation and Geo Server) the location information about the enemies operating around the ship. The Doctrine Authoring requires doctrine rules from the Experiment Control and provides them to the other components (Geo Server,Doctrine Validation, and Doctrine Reasoning) that require rules to take actions. Using the doctrine rules and track information from its environment, the Geo Server provides to the Doctrine Reasoning the precisely calculated region information for enemies. Lastly, the Doctrine Reasoning makes the decision of which task(s) to take against the enemies.
[Allen and Garlan, 1996] Allen, R. and Garlan, D. (1996). A case study in architectural modelling: The aegis system. In Proceedings of the Eighth International Workshop on Software Specification and Design (IWSSD-8), pages 6���15, Paderborn, Germany.
[Allen and Garlan, 1997] Allen, R. and Garlan, D. (1997). A formal basis for architectural connection. ACM Trans. Softw. Eng. Methodol., 6(3):213���249.
The translated ProMeLa code from the SAw-UML specification of aegis: