Description:
The Exclusive Write property says that no two writers may be accessing the shared data at the same time. This ensures that access to the shared data is mutually exclusive.
The writers all behave in a symmetric way with regard to the central data server. Due to this, it is sufficient to check this property for only two writers. If these two writers access the data in a mutually exclusive fashion, then all pairs of writers will. This property is specified in terms of writer 1 and writer 2. This allows the same property specification to be used when the problem is scaled.
This property should be valid when analyzed by any of the finite state verification tools.
Specification:
Back to Readers/Writers
Back to main