Most software systems are concerned with concurrent systems and thus it is of paramount importance to provide good formal support to the specification, design, and implementation of concurrent systems. Algebraic/logic methods have also found interesting applications in this field, especially to treat at the right level of abstraction the relevant features of a system, helping to hide the unnecessary details and thus to master system complexity. Due to the particularly complex nature of concurrent systems, and contrary to the case of classical (static) data structures, there are different ways of exploiting algebraic methods in concurrency. In the literature, we can distinguish at least four kinds of approaches. The algebraic techniques are used at the metalevel, for instance, in the definition or in the use of specification languages. Then a specification involves defining one or more expressions of the language, representing one or more systems. A particular specification language (technique) for concurrent systems is complemented with the possibility of abstractly specifying the (static) data handled by the systems considered using algebraic specifications. We can qualify the approaches of this kind by the slogan "plus algebraic specifications of static data types". These methods use particular algebraic specifications having "dynamic sorts", which are sorts whose elements are/correspond to concurrent systems. In such approaches there is only one "algebraic model" (for instance, a first-order structure or algebra) in which some elements represent concurrent systems. We can qualify the approaches of this kind as "algebraic specifications of dynamic-data types", which are types of dynamic data. These methods allow us to specify an (abstract) data type, which is dynamically changing with time. In such approaches we have different "algebraic" models corresponding to different states of the system. We can qualify the approaches of this kind as "algebraic specifications of dynamic data-types"; here the data types are dynamic. We have organized the paper around the classification above, providing significant illustrative examples for each of the classes. Our rationale has been mainly to present representatives. In particular, there is no intention of providing a comparative study of the methods. This is a goal outside the scope of the book. We use a common example for the presentation of all approaches, a very simple concurrent system.
File in questo prodotto:
Non ci sono file associati a questo prodotto.