Specification-oriented semantics for communicating processes

DOI10.1007/BF00268075zbMath0569.68019MaRDI QIDQ1060838

Ernst-Ruediger Olderog, C. A. R. Hoare

Publication date: 1986

Published in: Acta Informatica (Search for Journal in Brave)

zbMATH Keywords

correctnessdenotational semanticsspecificationliveness propertiescommunicating processesspecification-oriented semantics

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Theory of operating systems (68N25)

Related Items

A hierarchy of domains for real-time distributed computing, Factorizing proofs in timed CSP, A fully abstract trace model for dataflow and asynchronous networks, On the specification of elementary reactive behaviour, Ernst-Rüdiger Olderog: A Life for Meaning, Structure Preserving Bisimilarity, Supporting an Operational Petri Net Semantics of CCSP, Mediator Synthesis in a Component Algebra with Data, Infinite streams and finite observations in the semantics of uniform concurrency, On the operational semantics of nondeterminism and divergence, Quantales, observational logic and process semantics, Compositional failure-based semantic models for basic LOTOS, Responsiveness and stable revivals, Applications of compactness in the Smyth powerdomain of streams, Transition systems, metric spaces and ready sets in the semantics of uniform concurrency, A state-based approach to communicating processes, Conflict-preserving abstraction of discrete event systems using annotated automata, Two-thirds simulation indexes and modal logic characterization, Interpretations of recursion under unbounded nondeterminacy, Hiding in stream semantics of uniform concurrency, An application of temporal projection to interleaving concurrency, Order algebras: a quantitative model of interaction, Processes with infinite liveness requirements, A linear-time branching-time perspective on interface automata, Towards a complete hierarchy of compositional dataflow models, An algebraic approach to temporal logic, Unnamed Item, Notes on the methodology of CCS and CSP, Axiomatizing flat iteration, Just testing, Synchronous development of asynchronous systems, On the use of MTBDDs for performability analysis and verification of stochastic systems., Branching vs. Linear Time: Semantical Perspective, Reactive bisimulation semantics for a process algebra with timeouts, A partial ordering semantics for CCS, Comparative metric semantics for concurrent PROLOG, Step semantics for ``true concurrency with recursion, Towards a foundation for semantics in complete metric spaces, Correctness of concurrent processes, On deciding some equivalences for concurrent processes, Behavioural equivalence for infinite systems — Partially decidable!, Adequacy-preserving transformations of COSY path programs, The \({\mathcal NU}\) system as a development system for concurrent programs: \(\delta{\mathcal NU}\), Structured operational semantics and bisimulation as a congruence, Integrating a formal method into a software engineering process with UML and Java, From algebra to operational semantics, A hierarchy of failures-based models: theory and application, On cool congruence formats for weak bisimulations, Algebraic characterizations of trace and decorated trace equivalences over tree-like structures, On Synchronous and Asynchronous Interaction in Distributed Systems, Unnamed Item, Modal logics for communicating systems, Ready simulation for concurrency: it's logical!, Step failures semantics and a complete proof system, Dynamic and formal verification of embedded systems: A comparative survey, Divergence in testing and readiness semantics, Asynchronous communication of Petri Nets and the refinement of transitions, Modular specification of process algebras, Processes with local and global liveness requirements, Revivals, stuckness and the hierarchy of CSP models, (Bi)simulations up-to characterise process semantics, Abstract interface behavior of object-oriented languages with monitors, A note on the notation of recursion in process algebras, The fixed point theory of unbounded non-determinism, Basic observables for processes, Remarks on Testing Probabilistic Processes, On deciding trace equivalences for processes, The connection between an event structure semantics and an operational semantics for TCSP

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• A linear-history semantics for languages for distributed programming
• Calculi for synchrony and asynchrony
• A more complete model of communicating processes
• Algebra of communicating processes with abstraction
• Semantics of nondeterminism, concurrency, and communication
• A calculus of communicating systems
• A proof technique for communicating sequential processes
• Algebraic semantics
• A calculus of total correctness for communicating processes
• Power domains
• Testing equivalences for processes
• Linear time and branching time semantics for recursion with merge
• Predicative programming Part I
• A Theory of Communicating Sequential Processes
• Algebraic laws for nondeterminism and concurrency
• Acceptance trees
• Readies and Failures in the Algebra of Communicating Processes
• A Proof System for Communicating Sequential Processes
• Proving Liveness Properties of Concurrent Programs
• Formal Justification of a Proof System for Communicating Sequential Processes
• Formal verification of parallel programs
• Initial Algebra Semantics and Continuous Algebras
• Communicating sequential processes
• Processes and the denotational semantics of concurrency