DocumentCode
3439014
Title
Verifying networks of processes that synchronize via shared variables
Author
Kapus, Tatjana ; Horvat, Bogomir
Author_Institution
Fac. of Tech. Sci., Maribor Univ., Yugoslavia
fYear
1991
fDate
13-16 May 1991
Firstpage
113
Lastpage
117
Abstract
An approach to modeling and verification for networks of processes that synchronize solely via shared variables is presented. A process or a network is defined by its set of possible behaviors. Each behavior is an abstraction of an infinite execution sequence of the process. The specification of a network can be obtained naturally from the specifications of its component processes. It is possible to verify liveness properties by using standard temporal logic operators
Keywords
concurrency control; formal specification; multiprocessing programs; multiprocessing systems; synchronisation; temporal logic; component processes; infinite execution sequence; liveness properties; shared variables; specification; synchronisation; temporal logic operators; verification; Formal specifications; Interleaved codes; Logic; Postal services; Safety; State-space methods;
fLanguage
English
Publisher
ieee
Conference_Titel
CompEuro '91. Advanced Computer Technology, Reliable Systems and Applications. 5th Annual European Computer Conference. Proceedings.
Conference_Location
Bologna
Print_ISBN
0-8186-2141-9
Type
conf
DOI
10.1109/CMPEUR.1991.257366
Filename
257366
Link To Document