Issue No. 09 - September (2005 vol. 31)
DOI Bookmark: http://doi.ieeecomputersociety.org/10.1109/TSE.2005.104
Scenario-based requirements specifications are the industry norm for defining communication protocols. However, such scenarios often contain race conditions. A race condition occurs when events are specified to occur in a particular order, but in practice, this order cannot be guaranteed. The paper considers UML/MSC scenarios that can be described with standard partial order theoretic asynchronous behavioral semantics. We define these to be partial order scenarios. The paper proves there is a unique minimal generalization of a partial order scenario that is race free. The paper also proves there is a unique minimal race free refinement of the behavioral semantics of a partial order scenario. Unlike the generalization, the refinement cannot be realized in the form of a partial order scenario, although it can always be embedded in one. The paper also proves the results can be generalized to a subclass of iterative scenarios.
Index Terms- Requirements analysis, formal methods, distributed programming.
B. Mitchell, "Resolving Race Conditions in Asynchronous Partial Order Scenarios," in IEEE Transactions on Software Engineering, vol. 31, no. , pp. 767-784, 2005.