This Article 
   
 Share 
   
 Bibliographic References 
   
 Add to: 
 
Digg
Furl
Spurl
Blink
Simpy
Google
Del.icio.us
Y!MyWeb
 
 Search 
   
An Approach to Formal Specification of Control Modules
September 1980 (vol. 6 no. 5)
pp. 485-489
W.H. Leung, Bell Laboratories
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.
Index Terms:
state space model, Concurrent processes, control modules, input-output assertion, invariant assertion, program specification, resource sharing
Citation:
W.H. Leung, C.V. Ramamoorthy, "An Approach to Formal Specification of Control Modules," IEEE Transactions on Software Engineering, vol. 6, no. 5, pp. 485-489, Sept. 1980, doi:10.1109/TSE.1980.230789
Usage of this product signifies your acceptance of the Terms of Use.