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.
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.
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: https://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.
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 https://www.fipa.org/
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.