Verifiable abstractions for contract-oriented systems

DOI10.1016/J.JLAMP.2015.10.005zbMath1353.68194OpenAlexW2199920120MaRDI QIDQ347375

Alceste Scalas, Roberto Zunino, Massimo Bartoletti, Maurizio Murgia

Publication date: 30 November 2016

Published in: Journal of Logical and Algebraic Methods in Programming (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.jlamp.2015.10.005

zbMATH Keywords

verificationsession typescontract-oriented computingrewriting logic

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85) Grammars and rewriting systems (68Q42)

Related Items (5)

Composition of synchronous communicating systems ⋮ Session-based concurrency in Maude: executable semantics and type checking ⋮ Honesty by Typing ⋮ A fixed-points based framework for compliance of behavioural contracts ⋮ Input urgent semantics for asynchronous timed session types

Uses Software

• Maude
• CC-Pi
• Scribble

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Combining behavioural types with security analysis
• Maude: specification and programming in rewriting logic
• Twenty years of rewriting logic
• Subtyping for session types in the pi calculus
• Compliance and Subtyping in Timed Session Types
• Propositions as sessions
• On Global Types and Multi-Party Session
• On the Realizability of Contracts in Dishonest Systems
• Synthesising Choreographies from Local Session Types
• Deadlock-freedom-by-design
• Modelling and Verifying Contract-Oriented Systems in Maude
• Lending Petri Nets and Contracts
• Multiparty asynchronous session types
• Choreographies, Logically
• Using Higher-Order Contracts to Model Session Types (Extended Abstract)
• A Semantic Deconstruction of Session Types
• Compliance in Behavioural Contracts: A Brief Survey
• Global Progress in Dynamically Interleaved Multiparty Sessions
• A Theory of Design-by-Contract for Distributed Multiparty Interactions
• Session Types as Intuitionistic Linear Propositions
• Contract-Oriented Computing in CO2
• Linear type theory for asynchronous session types
• A Theory of Agreements and Protection
• Multiparty Compatibility in Communicating Automata: Characterisation and Synthesis of Global Session Types
• CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements

This page was built for publication: Verifiable abstractions for contract-oriented systems