Verifiable abstractions for contract-oriented systems
DOI10.1016/J.JLAMP.2015.10.005zbMATH Open1353.68194OpenAlexW2199920120MaRDI QIDQ347375FDOQ347375
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
Recommendations
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)
Cites Work
- Maude: specification and programming in rewriting logic
- On the realizability of contracts in dishonest systems
- Modelling and verifying contract-oriented systems in Maude
- Multiparty asynchronous session types
- A semantic deconstruction of session types
- Contract-oriented computing in CO\(_2\)
- Choreography synthesis as contract agreement
- 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
- Subtyping for session types in the pi calculus
- Combining behavioural types with security analysis
- Twenty years of rewriting logic
- Compliance and subtyping in timed session types
- The Maude LTL model checker
- An executable specification of asynchronous pi-calculus semantics and may testing in Maude 2.0
- Propositions as sessions
- On global types and multi-party sessions
- Synthesising Choreographies from Local Session Types
- Deadlock-freedom-by-design, multiparty asynchronous global programming
- Lending Petri nets and contracts
- Choreographies, logically
- Using higher-order contracts to model session types (extended abstract)
- 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
- Title not available (Why is that?)
- Linear type theory for asynchronous session types
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
- On the realizability of contracts in dishonest systems
- Runtime verification of contracts with Themulus
- Modelling and verifying contract-oriented systems in Maude
- Contract-oriented computing in CO\(_2\)
- Honesty by typing
- Probabilistic Contracts for Component-Based Design
Uses Software
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)
