vix.ing · top · new · best · stats · spec

Formalizing smart contract design patterns with DCR graphs

2026/05/21 by Mojtaba Eshghie, Wolfgang Ahrendt, Cyrille Artho +2 · 1 voice
Business, Management and Accounting · Computer Science · #Blockchain Technology Applications and Security #Business Process Modeling and Analysis #Multi-Agent Systems and Negotiation

paper · pdf · doi:10.1007/s10270-026-01366-w

openalex publication_date 2026/05/21 · openalex created_date 2026/05/22 · openalex updated_date 2026/07/29

Abstract

Abstract Smart contracts manage blockchain assets and embody business processes. Yet, mainstream languages lack explicit support for process concepts such as roles, action dependencies, and time constraints, leading to increased implementation complexity and analysis challenges. To address this, we use Dynamic Condition Response (DCR) graphs, a formal business process modeling language, to formalize the semantics of smart contract business logic. Modeling smart contracts in DCR graphs involves translating their underlying behavioral logic into a declarative visual model using DCR’s explicit constructs for events, roles, data, time, and inter-event relationships. Furthermore, we systematically model 15 common high-level smart contract design patterns , representing recurring solutions to business logic-level problems. These formalizations reduce ambiguity compared to informal descriptions and serve as language-independent specifications. We demonstrate the modeling process through three complete smart contract case studies that combine six design patterns. Our modeling methodology, formalizations, and correspondence between smart contract semantics and DCR graphs enable future automated analysis and verification.

Citations

Discussions

Related