Gerth, Rob; de Roever, W. P. Proving monitors revisited: A first step towards verifying object oriented systems. (English) Zbl 0617.68026 Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 9, 371-399 (1986). An axiomatic characterization of monitors, based on assumption-commitment style reasoning, is given that is sound and (relatively) complete. This characterization is based on the fundamental notions of cooperation and interference, but does not use them as second order notions. The cooperation test was originally conceived to capture the proof theoretical analogue of distributed message passing between processes, as opposed to the interference freedom test, being the proof theoretical analogue of concurrency based on interference by jointly shared variables. Since then, the cooperation test has been applied to characterize synchronous communication in Hoare’s Communicating Sequential Processes, Ichbia’s Ada and Wirth’s Modula-2, supported by soundness and completeness proofs. An overview is given of the rationale underlying this characterization, culminating in the development of proof systems for a new monitor based programming language for concurrency (Communicating Modules, CM) which combines distributed message passing between processes with interference through local variables of a process which are shared between its sub-processes. As such this is a first step towards the formal verification of object oriented systeme. In this context, we also show how the method, traditionally cauched in terms of proof outlines, can be rendered syntax directed in a precise and formal way. In a separate paper, the proof system has been shown to be sound and (relatively) complete. Cited in 6 Documents MSC: 68N25 Theory of operating systems Keywords:cooperation; interference; distributed message passing between processes; concurrency; shared variables; synchronous communication; Communicating Sequential Processes; Ada; Modula-2; soundness; completeness; Communicating Modules; formal verification of object oriented systeme Software:Modula; Ada95 PDFBibTeX XMLCite \textit{R. Gerth} and \textit{W. P. de Roever}, Ann. Soc. Math. Pol., Ser. IV, Fundam. Inf. 9, 371--399 (1986; Zbl 0617.68026)