Overview
On this page, you can find the two TBP specifications. The SessionManager example specifies a subsystem of an information system that takes care of the user authentication. The CoCoME example specifies an information system running in a supermarket chain. It models the individual cashdesks as well as the communication among the store and central server.
SessionManager
The architecture of the subsystem can be seen in the figure below. It consists of five components representing user interface, a logging component, a database, a component implementing the business logic, and finally a session manager. The entire subsystem forms a closed architecture meaning that such a composition does not provide any functionality, i.e., provided interfaces, to the outer world, and also does not require any functionality from other components, i.e., it does not feature any required interfaces that are not bound (connected to provided counterparts).
The application logic is implemented in the BusinesLogic component and the UserInterface component mediates the user input entering the system in form of http requests. The commands from the user, however, do not go directly to the business logic. The communication is intercepted by the SessionManger component that takes care about authentication of commands. The SessionManager requires some additional functionality provided by the Log and Database components. The Database component is used simultaneously by the BussinessLogic and SessionManager components.
The central part of this subsystem is the SessionManager component, which is a composed component; its architecture is depicted in the following figure:
Specification of SessionManager in TBP
CoCoME
We tested the capabilities of TBP on a model of a supermarket information system involving row of cashdesks, each featuring a number of devices (keyboard, credit card reader, etc.), and a central database of goods in the store. The model is taken over from the CoCoME contest assignment – www.
The architecture of the CoCoME application is depicted at the following figure.
CoCoME architecture
Flat CoCoME architecture
Since the current version of our tool does not support reasoning on refinement yet, to be able to verify the communication compatibility of particular components, we have flattened the application, i.e., removed the higher-level components and wiring just those ones on the lowest level. The resulting architecture can be seen here:
Specification of CoCoME in TBP
The entire sepcification can be downloaded by using the link below; it contains TBP specification of each CoCoME component as well as files describing wiring of their provided and required interfaces. The specification has been validated, no communication errors have been found.