Speaker: Jim Woodcock
Abstract: Orc is a lightweight orchestration language for composing distributed services, increasingly relevant to intelligent connected vehicles (ICVs), where coordination, latency, and failure handling demand rigorous reasoning about true concurrency. This talk proposes a semantics for Orc based on bi-Concurrent Kleene Algebra (bi-CKA) interpreted over pomsets (partial-order models of events). The algebra provides parallel (‖), sequencing (·), algebraic choice (+), (sequential) Kleene star (∗), and the exchange law, enabling compositional proofs that respect causal independence rather than interleavings. We provide denotations for the structural core (parallel, run-after/then, and atomic site calls), while publication-dependent combinators (bind, otherwise, and pruning) are specified operationally. We also demonstrate how modest algebraic enrichment (tests and preemption) yields a fully denotational treatment. On ICV scenarios (e.g., safe single-lane bridge crossing), the exchange law justifies refactoring parallel-then-sequentialpatterns into parallel pipelines, aiding optimisation and safety and liveness arguments. The framework cleanly isolates advisory LLM sidecar components, ensuring that adding human-facing explanations cannot compromise the verified plan’s behaviour, thereby supporting an auditable safety case. We outline links to Institutions and UTP, as well as a path to mechanisation in Lean. Overall, bi-CKA over pomsets supplies a mathematically transparent, true-concurrency backbone for Orc that scales to realistic orchestration tasks in safety-critical autonomy.
Bio: Jim Woodcock is a Professor of Software Engineering at the University of York and a Fellow of the Royal Academy of Engineering. His research focuses on formal methods, software engineering, and system verification, with contributions to Z notation, CSP, and unifying theories of programming. He played a key role in the formalization of IBM’s CICS transaction processing system, which won the Queen’s Award for Technological Achievement, and the Mondex electronic payment system, achieving the highest ITSEC classification. He has held academic positions at Oxford, Kent, and York and is the Editor-in-Chief of Formal Aspects of Computing.