Title :
Verifying networks of processes that synchronize via shared variables
Author :
Kapus, Tatjana ; Horvat, Bogomir
Author_Institution :
Fac. of Tech. Sci., Maribor Univ., Yugoslavia
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;
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
DOI :
10.1109/CMPEUR.1991.257366
