Realizability and verification of MSC graphs

DOI10.1016/J.TCS.2004.09.034MaRDI QIDQ1770427zbMATH OpenOpenAlexFDO

Authors Rajeev Alur, Kousha Etessami, Mihalis Yannakakis

Publication date 6 April 2005

Published in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL https://repository.upenn.edu/cis_papers/94

zbMATH Keywords

Software specificationFormal verificationMessage sequence charts

Mathematics Subject Classification ID

Graph theory (including graph drawing) in computer science (68R10) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Specification and verification (program logics, model checking, etc.) (68Q60)

Recommendations

• scientific article; zbMATH DE number 1754635
• Realizability of graph specifications: characterizations and algorithms
• Realizability of graphs
• Realizability of graphs and linkages
• Practical algorithms for MSO model-checking on tree-decomposable graphs
• Realizability Criteria for Compositional MSC
• scientific article; zbMATH DE number 5587270
• Realizability of fault-tolerant graphs
• Realizability and uniqueness in graphs

Cites work

• scientific article; zbMATH DE number 1670862 (Why is no real title available?)
• scientific article; zbMATH DE number 1927562 (Why is no real title available?)
• scientific article; zbMATH DE number 2086413 (Why is no real title available?)
• scientific article; zbMATH DE number 1418329 (Why is no real title available?)
• Membership problems for regular and context-free trace languages
• The complexity of satisfiability problems

Cited in

(26)

• Synthesis of Safe Message-Passing Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• scientific article; zbMATH DE number 1754635 (Why is no real title available?)
• Checking MSC specifications for timing inconsistency
• Branching pomsets: design, expressiveness and applications to choreographies
• Local Testing of Message Sequence Charts Is Difficult
• scientific article; zbMATH DE number 5587270 (Why is no real title available?)
• Realizable temporal logics for web service choreography
• Quantifying the Discord: Order Discrepancies in Message Sequence Charts
• Products of Message Sequence Charts
• Infinite-state high-level MSCs: model-checking and realizability
• A centralized and a decentralized method to automatically derive choreography-conforming web service systems
• Strong Safe Realizability of Message Sequence Chart Specifications
• Foundations of Software Science and Computation Structures
• On deciding synchronizability for asynchronously communicating systems
• QUANTIFYING THE DISCORD: ORDER DISCREPANCIES IN MESSAGE SEQUENCE CHARTS
• scientific article; zbMATH DE number 1927562 (Why is no real title available?)
• scientific article; zbMATH DE number 1754636 (Why is no real title available?)
• Timed runtime monitoring for multiparty conversations
• Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types
• Verification of scenario-based specifications using templates
• A calculus of global interaction based on session types
• Realizability Criteria for Compositional MSC
• Complete multiparty session type projection with automata
• Branching Pomsets for Choreographies
• Foundations of Software Science and Computational Structures

This page was built for publication: Realizability and verification of MSC graphs

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