What BRiCoS is
Concurrency is difficult because “what happens” is not a single sequence of steps. Many behaviours are possible, and the system’s correctness depends on subtle details: ordering, interference, partial failure, and resource constraints. A BRiCoS-style approach emphasises two ideas: (1) define small behavioural building blocks with clear interfaces, and (2) define composition operators that preserve meaning so you can reason about the whole system from its parts.
In practice, that often means writing down a behavioural model (an operational semantics, a transition system, or a protocol description), then pairing it with properties of interest: safety (“bad things never happen”), liveness (“good things eventually happen”), and compatibility (“these components can be connected without violating assumptions”). The point is not to force every system into heavy proofs, but to keep the reasoning surface clean enough that lightweight checks and modelling are feasible.
Why it matters
When a system is built from components, correctness is rarely local. Two components can be correct in isolation and still fail once composed. Typical reasons include incompatible expectations about scheduling, retry behaviour, timeouts, or message ordering. Rigorous building blocks help because they make these expectations explicit and provide a vocabulary for discussing them.
A second benefit is communication: models and contracts are documentation that can be checked. Even a small “protocol sketch” can prevent entire classes of misunderstandings by making it clear which interactions are intended and which are impossible.
Key concepts (glossary)
- Behavioural interface An interface that specifies not just data shapes, but interaction: ordering, choices, and allowed concurrency.
- Assume / guarantee A contract style that separates what a component requires from what it promises, enabling compositional reasoning.
- Composition operator A way to connect components (parallel, synchronisation, restriction) with a well-defined effect on behaviour.
- Refinement A relationship between models where an implementation is allowed fewer behaviours (or is more constrained) than a spec.
- Invariant A property intended to hold in every reachable state; useful both for proofs and for lightweight checks.
- State space The set of reachable configurations of a model. Its size drives the feasibility of exhaustive checking.
- Abstraction A simplification that preserves the properties you care about, used to keep checking tractable.
- Compatibility A notion that components can be connected without violating each other’s assumptions.
Diagram
A simple sketch: building blocks connect via explicit glue and checked properties.
Related work (internal)
This section intentionally links only within the site. If you want external bibliographic lists, use the external profiles box on /simon/.
- Behavioural contractsAssumptions/guarantees and composition failures.
- Session types and protocolsHow protocol structure supports safe interaction.
- Model checking primerState exploration as a check for behavioural models.
Further reading (internal)
- Publications hubPublication summaries grouped by type.
- Projects hubBRiCoS and adjacent projects with internal reading paths.