An Approach to Formal Specification of Control Modules
Wing Hong Leung, C. V. Ramamoorthy · IEEE Transactions on Software Engineering · 1980
This paper is concerned with the formal specification of program modules which control access to resources shared among concurrent proceses. The concept of state space is defined for such program modules and the formal specification is given in terms of a program module invariant and input-output assertions defined on the state space. Examples are provided to ilustrate the construction of sDecifications with this approach.