| The divide and conquer approach of recent software design techniques is well supported by UML-RT. It appears to be well suited to formal compositional verification. Since UML-RT is mainly used to design highly predictable and safety critical software, automated verification seems even more appealing. However, very few automated verification features can be found in today's design tools.This research proposes a method to verify the conformance of a capsule's behavioural state machine to the protocol state machine(s) implemented by its port(s). Although work on protocol conformance can be found in various software engineering fields, it has never been applied to UML-RT and has remained mostly theoretical. A tool has been created to enable this verification on an actual modeling tool which has been validated using sample UML-RT models.Keywords: UML, Protocol State Machine, Conformance, Verification, Model Checking.One way of improving predictability of a system expressed using UML-RT is by ensuring its capsules are compatible. Currently, capsule interfaces, called ports, are typed by protocols which define the signal name, data type and direction. However, it is possible to define a stronger notion of type using protocol state machines which specify the allowed message sequences. If we can verify pre-runtime that protocols are honoured for all possible executions, capsules proven conformant to the same protocol will have a higher level of compatibility. |
