An axiomatic semantics for nested concurrency.

*(English)*Zbl 0594.68026Summary: We give transformation rules for the concurrent parts of Hoare’s language CSP, transforming concurrent CSP programs into nondeterministic, sequential programs. On the basis of these transformations we define an axiomatic semantics for CSP with nested concurrency. This axiomatic system includes a rule for binary, associative process composition, enabling modular verification dealing with parts of concurrent systems as well as full programs. The proof system is fully abstract, in the sense that the internal structure of processes is irrelevant in the specification inasmuch it is not externally observable. An outline of a verification of a recursive, concurrent sorter is given as an example.

##### MSC:

68N25 | Theory of operating systems |

##### Keywords:

transformation rules; Hoare’s language CSP; concurrent CSP programs; axiomatic semantics; nested concurrency; process composition; modular verification##### Software:

Ada95##### References:

[1] | C. A. R. Hoare,Communicating sequential processes.Communications of the ACM, 21(8): 666–677, 1978. · Zbl 0383.68028 |

[2] | Reference Manual for the Ada Programming Language. U.S. Department of Defence, January 1983. ANSI/MIL-STD-1815A. |

[3] | Ralph Johan R. Back and R. Kurki-Suonio.Decentralization of process nets with centralized control. In 2nd ACM SIGACT-SIGOPS Symposium on Principles of Distributed Computing, 1983. |

[4] | Neelam Soundararajan and Ole-Johan Dahl.Partial Correctness Semantics of CSP. Research Report 66, Institute of Informatics, University of Oslo, February 1982. |

[5] | Krzysztof R. Apt, Nissim Frances and Willem P. de Roever,A proof system for communicating sequential processes. ACM Transactions on Programming Languages and Systems, 3(2), July 1980. · Zbl 0468.68023 |

[6] | G. M. Levin and D. Gries,A proof technique for communicating sequential processes.Acta Informatica, 15: 281–302, 1981. · Zbl 0463.68034 |

[7] | Stephen A. Cook,Soundness and completeness of an axiom system for program verification.SIAM Journal on Computing, 7: 70–90, 1978. · Zbl 0374.68009 |

[8] | Ole-Johan Dahl,Time Sequences as a Tool for Describing Program Behaviour. Research Report 48, Institute of Informatics, University of Oslo, August 1979. · Zbl 0456.68017 |

[9] | Ole-Johan Dahl,Can program proving be made practical? In M. Amirchachy and D. Neel, editors,Les Fondement de la Programmation, pages 56–115, CCE-CREST, IRIA, December 1977. Also in: Research report 33, Institute of Informatics, University of Oslo. |

[10] | Sigurd Meldal,An axiomatic semantic of access type tasks in Ada. Presented at the meeting of Ada Europe – Working Group on Formal Methods, February 6th 1986. · Zbl 0594.68026 |

[11] | Sigurd Meldal,Language Elements for Hierarchical Abstraction. Research Report 102, Institute of Informatics, University of Oslo, March 1986. · Zbl 0594.68026 |

This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.