DocumentCode
751645
Title
An Approach to Formal Specification of Control Modules
Author
Leung, Wu Hon ; Ramamoorthy, C.V.
Author_Institution
Bell Laboratories
Issue
5
fYear
1980
Firstpage
485
Lastpage
489
Abstract
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.
Keywords
Concurrent processes; control modules; input-output assertion; invariant assertion; program specification; resource sharing; state space model; Formal specifications; Laboratories; Monitoring; Process control; Programming profession; Protection; Resource management; State-space methods; Concurrent processes; control modules; input-output assertion; invariant assertion; program specification; resource sharing; state space model;
fLanguage
English
Journal_Title
Software Engineering, IEEE Transactions on
Publisher
ieee
ISSN
0098-5589
Type
jour
DOI
10.1109/TSE.1980.230789
Filename
1702765
Link To Document