XCD - An Architecture Description Language
Software architecture description languages (ADL) have been proposed as a way to properly specify the architectures of complex software systems, in a way that allows both communication among the different stakeholders and an early analysis of these systems for a number of properties. However, practitioners seem to have shunned the ADL developed in academia and mainly use other modeling languages, that were not originally created for describing architectures. In a recent survey, practitioners have expressed a wish for analyzing their architectures (esp. for non-functional properties) and at the same time expressed their dissatisfaction with existing ADL, finding that the formal notations they use have a learning curve that they perceive as being too steep.
We propose a new ADL, called XCD, that attempts to address these issues. To this end, XCD is a formal language, allowing the formal analysis of systems. In its current form, it focuses on safety and liveness properties (deadlocks, etc.), leaving support for non-functional properties, such as reliability or performance, for later. In order to avoid imposing a steep learning curve on practitioners, XCD follows a Design-by-Contract (DbC) approach. DbC has the advantage of allowing practitioners to express formal models in a notation that resembles the programming languages they use. DbC has in fact already been embraced by practitioners, who so far use it mainly for improving their testing methods. XCD specifications can be translated to ProMeLa so as to verify that (i) provided services local interaction constraints are satisfied, (ii) provided services functional pre-conditions are complete, (iii) there are no race-conditions, (iv) event buffer sizes suffice, and (v) there is no global deadlock. Without formally analyzable architectures errors can remain undiscovered for a long time and cost too much to repair.
Visual XCD has just been released - click
XCD's Evolution
XCD builds on our earlier attempts at developing such an architecture description language. In our early work, XCD was influenced more from BIP’s separation of behaviour, interaction, and control, and thereby introduced three main architectural elements: components, connectors, and control strategies (papers 1 to 4). Control strategies are essentially extra role constraints specified externally to the connector roles, allowing to experiment with different design solutions without modifying connectors. Moreover, I used the Finite State Process (FSP) process algebra to define the formal mapping of XCD elements that allows formal verification via the LTSA model checker.
Our publications [4,5,9,10,11] have been produced from our initial work.
In our final work, we have simplified the main notions, no longer having "control strategies" – they can already be represented by connectors. Moreover, we have extended the language to better support designers (e.g. enumerated types, interval values, helper functions, asynchronous interaction, or indeed composite components that were not supported in my initial FSP encoding and tool). I have also replaced FSP with SPIN’s ProMeLa language, as encoding asynchronous interaction and method/event parameters in FSP required too much effort. SPIN has also a more powerful model checker than FSP’s LTSA – partly because it does not attempt to construct the state-space of each process as it is defined but only does so on-the-fly, as needed. SPIN’s code availability also helped us in better understanding the use of some constructs and slightly optimising my models.
Our publications [1,2,3,6,7,8] have been produced from our final work.
XCD's Translation tool
XCD's translation tool performs the following operations for a given XCD architecture specification. It firstly checks for the syntactical correctness. Then, if no syntax error is found, the tool checks whether the XCD architecture is well-defined or not. If the XCD architecture is well-defined, then, the tool translates the syntactically correct and well-defined XCD architecture into a ProMeLa model.
The latest version of the tool can be downloaded from here.
Instructions for running the tool:
1- Download and install SPIN from its website : http://spinroot.com/spin/whatispin.html.
2- Download and install the XCD tool (xcd.jar) from the above given link.
3- Save your XCD specification into a file with ".xcd" extension.
4- Place the tool jar file inside the same directory as your specification file, and then, run the command
"java -jar xcd.jar fileName.xcd".
This command produces a folder "src-gen" which includes a set of ProMeLa files representing the ProMeLa model of your XCD specification.
5- Run either ISPIN GUI of SPIN or use command line.
If ispin is used, you need to input the
"configuration.pml" file of the "src-gen"
It corresponds to the system configuration that you are supposed to speficfy as part of your XCD specification.
6- If you use command line, use the following SPIN verification commands for verifying the "configuration.pml".
$ spin -a configuration.pml
$ gcc -O2 -DMEMLIM=7024 -o pan pan.c
$ ./pan
For more information about using SPIN for verifying ProMeLa models, please refer to the http://spinroot.com/spin/Man/Roadmap.html
Some Applications of XCD
XCD and its tool have been used to specify and verify a number of real-system case studies. Below, we give the XCD architecture specifications and the translated ProMeLa models of these case-studies.
Gas Station
We consider here the classic architectural case study of a gas station [NACO97] 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. [NACO97] G. Naumovich, G. S. Avrunin, L. A. Clarke, L. J. Osterweil. Applying Static Analysis to Software Architectures. In Jazayeri and Schauer (eds.), ESEC / SIGSOFT FSE. Lecture Notes in Computer Science 1301, pp. 77���93. Springer, 1997.
Click for the XCD Specification (Chaos -- wrong use of component services)
Click for the transformed ProMeLa Model (chaos)
Click for the XCD Specification (Avoiding chaos)
Click for the transformed ProMeLa Model (Avoiding chaos)
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.
Click for the XCD Specification (Deadlocking)
Click for the transformed ProMeLa Model (Deadlocking)
Click for the XCD Specification (Deadlock-free)
Click for the transformed ProMeLa Model (Deadlock-free)
Lunar Lander System
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 [Taylor et al.(2010)Taylor, Medvidovic, and Dashofy]. 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. [Maoz et al.(2013)] Shahar Maoz, Jan Oliver Ringert, and Bernhard Rumpe. Synthesis of component and connector models from crosscutting structural views. In Bertrand Meyer, Luciano Baresi, and Mira Mezini, editors, ESEC/SIGSOFT FSE, pages 444���454. ACM, 2013. ISBN 978-1-4503-2237-9. Evaluation Material Example Models and Specifications, URL: http://www.se-rwth.de/materials/cncviews/ [Taylor et al.(2010)] Richard N. Taylor, Nenad Medvidovic, and Eric M. Dashofy. Software Architecture - Foundations, Theory, and Practice. Wiley, 2010. ISBN 978-0-470-16774-8.
Click for the XCD Specification (Event buffer overflow)
Click for the transformed ProMeLa Model
Click for the XCD Specification zip -- all configurations
Click for the XCD Specification (Avoiding event buffer overflow)
Click for the transformed ProMeLa Model (Avoiding event buffer overflow)
FIPA English Auction Protocol
English auction interaction protocol has been specified by the members of the FIPA [FIPA] describing a marketplace with an auctioneer who uses the English auction variant to sell an item. As shown in the figure, its structure comprises an initiator interacting with a set of participants. The auction is started by the initiator informing all the participants (inform-start-of-auction). Then, the initiator calls the participants for their participation to the auction (cfp). Each participant then makes a bid for the good (propose) which is either accepted (accept_proposal) if the proposed price is greater than the current price or rejected (reject_proposal) by the initiator if it is less than the current price. Once a bid is accepted, the initiator updates the current price with the price of the accepted bid. The initiator keeps calling the participants for their participation until everyone rejects the updated price of the good which indicates that the auction ends at that point (inform-end-of-auction). [FIPA] FIPA: http://www.fipa.org/. Click for the XCD Specification (Deadlocking)
Click for the transformed ProMeLa Model (Deadlocking)
Nuclear Power Plant System
Alur etal. [Alur et al., 2003] described an un-realisable MSC representing a simplified nuclear power plant, shown in the above figure. The interaction therein involves an Incrementor and a Doubler client updating the amounts of Uranium fuel (UR) and Nitric Acid (NA) in a nuclear reactor. After the update operations, the amounts of UR and NA must be equal to avoid any nuclear accident. The interaction of the two clients with the NA and UR variables, can easily be specified ADLs suporting complex connectors, e.g., Wright. However, this specification is un-realisable as Alur has shown because it is impossible to implement it in a decentralised manner in a way that avoids behaviours excluded by the glue. Indeed, developers implementing such connector specifications have to either introduce a centralised unit for the glue part which can never be possible for distributed cases, or distribute glue behaviour into roles which may not necessarily be possible. Using XCD, designers can specify the Alur's plant system and detect by verifying the transformed ProMeLA model that its constraint (i.e., the amounts of UR and NA must be equal) cannot be met by the system. However, one can introduce a controller component that sits among the Alur's plant components and control their interaction. So, we give here a decentralised specification of Alur (without a controller) and also a centralised specification of it (with a controller to meet the constraint). Moreover, we further give the property specification in ProMeLa which describes Alur's constraint.
[Alur et al., 2003] Alur, R., Etessami, K., and Yannakakis, M. (2003). Inference of message sequence charts. IEEE Trans. Software Eng., 29(7):623���633.
Click for the Decentralised XCD Specification
Click for the transformed ProMeLa Model -- Decentralised
Click for the Centralised XCD Specification