Modelling and verifying contract-oriented systems in Maude

DOI10.1007/978-3-319-12904-4_7MaRDI QIDQ2945134zbMATH OpenOpenAlexFDO

Authors Massimo Bartoletti, Maurizio Murgia, Alceste Scalas, Roberto Zunino

Publication date 9 September 2015

Published in Rewriting Logic and Its Applications (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-12904-4_7

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Grammars and rewriting systems (68Q42) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Verifiable abstractions for contract-oriented systems
• Contract-oriented computing in CO₂
• On the realizability of contracts in dishonest systems
• Honesty by typing
• Model Checking Contracts – A Case Study

Cited in

(8)

• Contracts as games on event structures
• On the realizability of contracts in dishonest systems
• Verifiable abstractions for contract-oriented systems
• Contract-oriented computing in CO₂
• Verifying liquidity of recursive bitcoin contracts
• Model checking strategy-controlled rewriting systems
• Session-based concurrency in Maude: executable semantics and type checking
• Combining behavioural types with security analysis

Describes a project that uses

Uses Software

• Maude

This page was built for publication: Modelling and verifying contract-oriented systems in Maude

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2945134)