Project index
Each item includes a short internal reading path.
BRiCoS
BRiCoS (Building Blocks for Rigorous Design of Concurrent Software) is a building-block perspective on concurrency. Instead of starting from a large language or a monolithic framework, it encourages small behavioural blocks with explicit composition operators. The motivation is compositional reasoning: being able to explain global system behaviour from local components and their glue.
The page on this site focuses on the vocabulary and the engineering consequences: how to describe boundaries, how to make assumptions explicit, and how to connect models to feasible checks. It is a representative example of the “model → property → check” loop described in the research hub.
- BRiCoS topic pageHigh-level description, glossary, and diagram.
- Behavioural contractsAssumptions and guarantees as compositional interfaces.
- Model checking primerA feasibility lens on checking behavioural models.
Behavioural contracts
Many integration failures are contract failures. The contract is not “the API signature”; it is the behaviour that the API assumes: ordering rules, error semantics, timeouts, and resource expectations. Behavioural contracts make those assumptions explicit and provide a language for compatibility: “these components can be connected without violating their assumptions”.
A key idea is assume/guarantee reasoning. It is useful because it is compositional: you can reason locally about a component, then derive what you can promise about the composed system. It also has a strong practical side: contracts can be checked at boundaries (tests, monitors, or lightweight models) and used as communication artefacts between teams.
- Note: behavioural contractsDefinitions, examples, and pitfalls.
- Research: component modelsWhy glue and composition matter.
- PublicationsShort summaries that motivate contract-based reasoning.
Component-based reasoning
Component-based reasoning is about bridging the gap between “component correctness” and “system correctness”. A component can be locally correct and still produce a faulty system after composition because assumptions do not match. A component model makes the interface and the glue explicit, giving you a place to attach checks and to define compatibility.
This site uses the BIP perspective as a useful mental model: separate behaviour from interaction and priority. Even when you are not using a specific framework, the separation is a practical design technique because it keeps coordination logic out of component internals.
- Note: component systems and BIPComponents, interactions, priorities.
- ICE 2011Workshop hub that centres on component composition and reasoning.
- Graph rewriting and SOSRules-as-semantics for structured models.
Session types & protocols
Protocols are a form of structure. In concurrent and message-driven systems, the hardest bugs are about interaction: which messages are allowed, in which order, and under which conditions. Session types treat that structure as a type-level object, enabling checks at compile time or at runtime boundaries.
The key idea is to model conversations rather than individual calls: branching, recursion, and concurrency. Even if you do not use a session type system directly, a protocol description can serve as a contract and as a shared design artefact.
- Note: session types and protocolsDefinitions, examples, and pitfalls.
- Research: behavioural typesHow protocols fit the wider themes.
- PublicationsSummaries that connect protocols to feasible workflows.