A logical approach for refinement of concurrent systems
|Title||A logical approach for refinement of concurrent systems|
|Publication Type||Technical Report|
|Authors||S. Yang, and J. W. Sanders|
|Year of Publication||2009|
We propose a formalism for modelling concurrent systems and for supporting stepwise refinement of concurrent systems. Our formalism allows one to describe the possible behaviours of a concurrent system in an operational manner, and to select from the operational description the desired behaviours using a logical approach. We discuss how our formalism can be used for incremental stepwise development where a high-level specification consisting of little operational aspect and largely logical assertions, is refined gradually into a low-lever specification consisting of mainly operational description and few or no logical dictations. We illustrate this refinement methodology with a simplified version of Lamportâ€™s Bakery algorithm.