Verifiable abstractions for contract-oriented systems

DOI10.1016/J.JLAMP.2015.10.005MaRDI QIDQ347375zbMATH OpenOpenAlexFDO

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

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

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

• Modelling and verifying contract-oriented systems in Maude
• On the realizability of contracts in dishonest systems
• Contract-oriented computing in CO₂
• Honesty by typing
• Contracts, games, and refinement.

Cites work

• scientific article; zbMATH DE number 1973125 (Why is no real title available?)
• A semantic deconstruction of session types
• A theory of agreements and protection
• A theory of design-by-contract for distributed multiparty interactions
• An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0
• CC-Pi: A Constraint-Based Language for Specifying Service Level Agreements
• Choreographies, logically
• Choreography synthesis as contract agreement
• Combining behavioural types with security analysis
• Compliance and subtyping in timed session types
• Compliance in behavioural contracts: a brief survey
• Contract-oriented computing in CO₂
• Deadlock-freedom-by-design, multiparty asynchronous global programming
• Global Progress in Dynamically Interleaved Multiparty Sessions
• Lending Petri nets and contracts
• Linear type theory for asynchronous session types
• Maude: specification and programming in rewriting logic
• Modelling and verifying contract-oriented systems in Maude
• Multiparty asynchronous session types
• Multiparty compatibility in communicating automata: characterisation and synthesis of global session types
• On global types and multi-party sessions
• On the realizability of contracts in dishonest systems
• Propositions as sessions
• Session types as intuitionistic linear propositions
• Subtyping for session types in the pi calculus
• Synthesising Choreographies from Local Session Types
• The Maude LTL model checker
• Twenty years of rewriting logic
• Using higher-order contracts to model session types (extended abstract)

Cited in

(11)

• Input urgent semantics for asynchronous timed session types
• Session-based concurrency in Maude: executable semantics and type checking
• Composition of synchronous communicating systems
• Probabilistic contracts for component-based design
• A fixed-points based framework for compliance of behavioural contracts
• Runtime verification of contracts with Themulus
• On the realizability of contracts in dishonest systems
• Modelling and verifying contract-oriented systems in Maude
• Contract-oriented computing in CO₂
• Honesty by typing
• Probabilistic Contracts for Component-Based Design

Describes a project that uses

Uses Software

• Scribble
• CC-Pi
• Maude

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

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