Specifying Software Systems with High Internal Concurrency Based on Actor Formalism

A specification technique for communicating parallel processes and concurrent computations based on actor formalism is presented. The use of a notion of states of actors (processes or modules) together with the partial ordering among events is central in our technique. This technique is not only powerful in specifying the behaviours of individual communicating parallel modules, but also powerful in specifying and verifying the behaviors of software systems, such as operating systems, which are characterized by concurrent activities of their subsystems. Some of its apllications to an existing operafing system are described in the Appendix. A method of defining states of individual actors (processes or modules) as mathematical functions is suggested.