Issue 6152: Protocol state machines are not pre/postconditions (uml2-superstructure-ftf) Source: NIST (Dr. Conrad Bock, conrad.bock(at)nist.gov) Nature: Revision Severity: Significant Summary: The text in the semantics of ProtocolStateMachine says: The protocol transition can always be translated into pre and post conditions of the associated operation. For example, the transition in Figure 9-13 specifies that: 1. the operation "m1" can be called on an instance when it is in the state S1 under the condition C1, 2. when m1 is called in the state S1 under the condition C1, then the final state S2 must be reached under the condition C2. The above translation is not possible by the definition of protocol machines. Protocol machines are a client-side view, independent of the the internal behavior machine of the instance. This means the protocol states are not necessarily the same as the internal states of the intance. The protocol machine is keeping track of the operations that have been called to enforce and order, but the internal behavior machine may or may not be the same. If they are the same, there would be no purpose to the protocol machine. The spec actually makes the same point at the beginning of the semantics of PSM: Using pre and post conditions on operations is a technique well suited for expressing such specifications. However, pre and post conditions are expressed at the operation level, and therefore do not provide a synthetic overview at the classifier level. Protocol state machines provide a global overview of the classifier protocol usage, in a simple formal representation. That is, If PSM's were easiy mappable to operation pre/postcondtions, there would be no point to having PSMs. Suggested change to the text: A protocol state machine could in theory be translated to pre- and postconditions on operations, but the conditions would need to account for the operation call history on the instance, which may or may not be straightforwardly represented by its internal states. A protocol machine provides a direct model of the state of interaction with the instance, so that constraints on interaction are more easily expressed. Resolution: see above Revised Text: Actions taken: August 30, 2003: received issue March 8, 2005: closed issue Discussion: OMG Issue No: 6150 NIST (Mr. Conrad Bock, conrad.bock@nist.gov conradb@cme.nist.gov) It is probably worthwhile to define a graphical syntax representing BehavioralFeature.method. This could take the form of either • showing the name of the instance of Behavior which is the method along in the compartment where the behavioral feature is exhibited • having a graphical link between the behavioral feature and a symbol representing the behavior instance (similar to how it is shown that a CollaborationOccurrence represents a Classifier (see Figure 106). The downside of either is that users typically don’t think of the behavioral feature and the behavior as separate things and usually would not dream of naming the behavior (of course, this is not required). In particular, if the behavior is described by a body string a convenient way of showing that body string with the behavioral feature would be desired. Today tools typically use the property sheet for the behavioral feature to show the associated behavior. There are already different vendor specific solutions for some behaviors as methods. We need to gain better experience before standardizing as solution. Disposition: Deferred End of Annotations:===== Name: Conrad Bock Company: NIST mailFrom: conrad.bock@nist.gov Nature: Revision Severity: Significant Subject: Protocol state machines are not pre/postconditions The text in the semantics of ProtocolStateMachine says: The protocol transition can always be translated into pre and post conditions of the associated operation. For example, the transition in Figure 9-13 specifies that: 1. the operation "m1" can be called on an instance when it is in the state S1 under the condition C1, 2. when m1 is called in the state S1 under the condition C1, then the final state S2 must be reached under the condition C2. The above translation is not possible by the definition of protocol machines. Protocol machines are a client-side view, independent of the the internal behavior machine of the instance. This means the protocol states are not necessarily the same as the internal states of the intance. The protocol machine is keeping track of the operations that have been called to enforce and order, but the internal behavior machine may or may not be the same. If they are the same, there would be no purpose to the protocol machine. The spec actually makes the same point at the beginning of the semantics of PSM: Using pre and post conditions on operations is a technique well suited for expressing such specifications. However, pre and post conditions are expressed at the operation level, and therefore do not provide a synthetic overview at the classifier level. Protocol state machines provide a global overview of the classifier protocol usage, in a simple formal representation. That is, If PSM's were easiy mappable to operation pre/postcondtions, there would be no point to having PSMs. Suggested change to the text: A protocol state machine could in theory be translated to pre- and postconditions on operations, but the conditions would need to account for the operation call history on the instance, which may or may not be straightforwardly represented by its internal states. A protocol machine provides a direct model of the state of interaction with the instance, so that constraints on interaction are more easily Reply-To: From: "Conrad Bock" To: "'UML Superstructure FTF'" Subject: RE: SM - Proposed resolution for PSM issues Date: Sun, 25 Jan 2004 01:10:08 -0500 X-Mailer: Microsoft Outlook IMO, Build 9.0.2416 (9.0.2910.0) Importance: Normal Phillipe, Thanks for the proposals. The explanation in 6490 (Protocol machines do not subset state invariant) is fine with me. On Issue 6152 (Protocol state machines are not pre/postconditions), change 1 looks good to me. Change 2 is better than the existing text, but still refers to "states" without clarifying whether they are internal or external. Since it is a PSM, and change 1 says PSM states are not generally easy to map to internal states, I'd suggest putting "PSM" before state in the text, and delete "final" before state because it shouldn't imply Final State. Here is the edit: Semantics of a protocol transition A protocol transition can be semantically interpreted in terms of pre and post conditions on the associated operation. For example, the transition in Figure 365 can be interpreted in the following way : 1. the operation "m1" can be called on an instance when it is in the PSM state S1 under the condition C1, 2. when "m1" is called in the PSM state "S1" under the condition "C1", then the PSM state "S2" must be reached under the condition "C2". Issue 6152: Protocol state machines are not pre/postconditions (uml2-superstructure-ftf) Click here for this issue's archive. Source: NIST (Mr. Conrad Bock, mailto:%20conrad.bock@nist.gov) Nature: Revision Severity: Significant Summary: The text in the semantics of ProtocolStateMachine says: The protocol transition can always be translated into pre and post conditions of the associated operation. For example, the transition in Figure 9-13 specifies that: 1. the operation "m1" can be called on an instance when it is in the state S1 under the condition C1, 2. when m1 is called in the state S1 under the condition C1, then the final state S2 must be reached under the condition C2. The above translation is not possible by the definition of protocol machines. Protocol machines are a client-side view, independent of the internal behavior machine of the instance. This means the protocol states are not necessarily the same as the internal states of the instance. The protocol machine is keeping track of the operations that have been called to enforce and order, but the internal behavior machine may or may not be the same. If they are the same, there would be no purpose to the protocol machine. The spec actually makes the same point at the beginning of the semantics of PSM: Using pre and post conditions on operations is a technique well suited for expressing such specifications. However, pre and post conditions are expressed at the operation level, and therefore do not provide a synthetic overview at the classifier level. Protocol state machines provide a global overview of the classifier protocol usage, in a simple formal representation. That is, If PSM's were easily mappable to operation pre/postcondtions, there would be no point to having PSMs. Suggested change to the text: A protocol state machine could in theory be translated to pre- and post-conditions on operations, but the conditions would need to account for the operation call history on the instance, which may or may not be straightforwardly represented by its internal states. A protocol machine provides a direct model of the state of interaction with the instance, so that constraints on interaction are more easily expressed. Disposition: 1 Change the text in Protocol state machine semantics from: --- Using pre and post conditions on operations is a technique well suited for expressing such specifications. However, pre and post conditions are expressed at the operation level, and therefore do not provide a synthetic overview at the classifier level. Protocol state machines provide a global overview of the classifier protocol usage, in a simple formal representation. Protocol state machines may not express all the pre- and postconditions of operations. In that case, additional pre- or postconditions can be added at the operation level. Formally, the pre condition of an operation will be the addition (logical "and") of the constraint defined as pre condition of the operation, if any, to the constraint deduced from the protocol state machine if any. The same applies to the post condition of an operation. --- To --- The states of a protocol state machine present an external view of the class that is exposed to its clients. They do not correspond necessarily to the internal states of the instances, as expressed by behavioral state machines. A protocol state machine expresses parts of the constraints that can be formulated for pre and post-conditions on operations. The translation from protocol state machine to pre and post conditions on operations might not be straightforward, because the conditions would need to account for the operation call history on the instance, which may or may not be directly represented by its internal states. A protocol state machine provides a direct model of the state of interaction with the instance, so that constraints on interaction are more easily expressed. 2 Change the text in protocol transition semantics from : --- Equivalences to pre and post conditions of operations The protocol transition can always be translated into pre and post conditions of the associated operation. For example, the transition in Figure 365 specifies that: 1. the operation "m1" can be called on an instance when it is in the state S1 under the condition C1, 2. when m1 is called in the state S1 under the condition C1, then the final state S2 must be reached under the condition C2. This can be translated into the following pre and post conditions of the operation m1 (Figure 365). Operation m1() Pre: S1 is in the configuration state and C1 Post: if the initial condition was .S1 is in the configuration state and C1. then S2 is in the configuration state and C2. --- To --- Semantics of a protocol transition A protocol transition can be semantically interpreted in terms of pre and post conditions on the associated operation. For example, the transition in Figure 365 can be interpreted in the following way : 1. the operation "m1" can be called on an instance when it is in the PSM state .S1. under the condition .C1., 2. when .m1. is called in the PSM state .S1. under the condition .C1., then the PSM state .S2. must be reached under the condition .C2.. --- Issue 6152: Protocol state machines are not pre/postconditions (uml2-superstructure-ftf) Click here for this issue's archive. Source: NIST (Mr. Conrad Bock, mailto:%20conrad.bock@nist.gov) Nature: Revision Severity: Significant Summary: The text in the semantics of ProtocolStateMachine says: The protocol transition can always be translated into pre and post conditions of the associated operation. For example, the transition in Figure 9-13 specifies that: 1. the operation "m1" can be called on an instance when it is in the state S1 under the condition C1, 2. when m1 is called in the state S1 under the condition C1, then the final state S2 must be reached under the condition C2. The above translation is not possible by the definition of protocol machines. Protocol machines are a client-side view, independent of the internal behavior machine of the instance. This means the protocol states are not necessarily the same as the internal states of the instance. The protocol machine is keeping track of the operations that have been called to enforce and order, but the internal behavior machine may or may not be the same. If they are the same, there would be no purpose to the protocol machine. The spec actually makes the same point at the beginning of the semantics of PSM: Using pre and post conditions on operations is a technique well suited for expressing such specifications. However, pre and post conditions are expressed at the operation level, and therefore do not provide a synthetic overview at the classifier level. Protocol state machines provide a global overview of the classifier protocol usage, in a simple formal representation. That is, If PSM's were easily mappable to operation pre/postcondtions, there would be no point to having PSMs. Suggested change to the text: A protocol state machine could in theory be translated to pre- and post-conditions on operations, but the conditions would need to account for the operation call history on the instance, which may or may not be straightforwardly represented by its internal states. A protocol machine provides a direct model of the state of interaction with the instance, so that constraints on interaction are more easily expressed. Disposition: 1 Change the text in Protocol state machine semantics from: --- Using pre and post conditions on operations is a technique well suited for expressing such specifications. However, pre and post conditions are expressed at the operation level, and therefore do not provide a synthetic overview at the classifier level. Protocol state machines provide a global overview of the classifier protocol usage, in a simple formal representation. Protocol state machines may not express all the pre- and postconditions of operations. In that case, additional pre- or postconditions can be added at the operation level. Formally, the pre condition of an operation will be the addition (logical "and") of the constraint defined as pre condition of the operation, if any, to the constraint deduced from the protocol state machine if any. The same applies to the post condition of an operation. --- To --- The states of a protocol state machine (protocol states) present an external view of the class that is exposed to its clients. Depending on the context, protocol states can correspond to the internal states of the instances as expressed by behavioral state machines, or be different. A protocol state machine expresses parts of the constraints that can be formulated for pre and post-conditions on operations. The translation from protocol state machine to pre and post conditions on operations might not be straightforward, because the conditions would need to account for the operation call history on the instance, which may or may not be directly represented by its internal states. A protocol state machine provides a direct model of the state of interaction with the instance, so that constraints on interaction are more easily expressed. 2 Change the text in protocol transition semantics from : --- Equivalences to pre and post conditions of operations The protocol transition can always be translated into pre and post conditions of the associated operation. For example, the transition in Figure 365 specifies that: 1. the operation "m1" can be called on an instance when it is in the state S1 under the condition C1, 2. when m1 is called in the state S1 under the condition C1, then the final state S2 must be reached under the condition C2. This can be translated into the following pre and post conditions of the operation m1 (Figure 365). Operation m1() Pre: S1 is in the configuration state and C1 Post: if the initial condition was .S1 is in the configuration state and C1. then S2 is in the configuration state and C2. --- To --- Semantics of a protocol transition A protocol transition can be semantically interpreted in terms of pre and post conditions on the associated operation. For example, the transition in Figure 365 can be interpreted in the following way : 1. the operation "m1" can be called on an instance when it is in the protocol state .S1. under the condition .C1., 2. when .m1. is called in the protocol state .S1. under the condition .C1., then the protocol state .S2. must be reached under the condition .C2.. --- expressed.