Enhanced Operational Semantics: A Tool for Describing and Analysing Concurrent Systems

This article surveys the definition and application of an enhancement of structural operational semantics in the field of concurrent systems, and also addresses issues of distribution and mobility of code. The focus is on how enriching the labels of transitions with encodings of their deduction trees is sufficient to derive qualitative and quantitative information on the systems in hand simply by relabeling the transitions of a unique concrete model. Categories and Subject Descriptors: D.3.1 [Programming Languages]: Formal Definitions and Theory-Semantics; C.2.4 [Computer-Communication Networks]: Distributed Systems; C.4 [Performance of Systems]: Modeling Techniques; D.2.1 [Software Engineering]: Requirements/Specifications; D.2.4 [Software Engineering]: Software/Program Verification; F.1.2 [Computation by Abstract Devices]: Modes of Computation-Interactive and reactive computation, Parallelism and concurrency; F.3.2 [Logics and Meanings of Programs]: Semantics of Programming Languages-Operational semantics