Aspects of formal and graphical design of a bus system

This study shows the derivation of a local segmented bus arbiter from an original single segment bus arbiter. The operations are performed in the formal framework of action systems and illustrated in a graphical manner using the corresponding action systems - UML profile notations. The derivation is useful both to demonstrate the capability of preserving correctness when considering an important hardware design decision and also to identify means through which this kind of decisions can be performed in a graphical environment.