Infinite-state high-level MSCs: model-checking and realizability

DOI10.1016/J.JCSS.2005.09.007MaRDI QIDQ2495403zbMATH OpenOpenAlexFDO

Authors Blaise Genest, Anca Muscholl, Helmut Seidl, Marc Zeitoun

Publication date 30 June 2006

Published in Journal of Computer and System Sciences (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.jcss.2005.09.007

zbMATH Keywords

communicating automataconcurrencyMSC model-checkingsynthesis

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)

Recommendations

• scientific article; zbMATH DE number 2086660
• From finite state communication protocols to high-level message sequence charts
• Safe realizability of high-level message sequence charts
• Realizability of high-level message sequence charts: closing the gaps
• Compositional message sequence charts

Cites work

• Developments in Language Theory
• Distributed controller synthesis for local specifications
• HMSCs as partial specifications . . . with PNs as completions
• scientific article; zbMATH DE number 2086239 (Why is no real title available?)
• scientific article; zbMATH DE number 2086413 (Why is no real title available?)
• scientific article; zbMATH DE number 2086660 (Why is no real title available?)
• Message sequence graphs and decision problems on Marzurkiewicz traces
• On Communicating Finite-State Machines
• On message sequence graphs and finitely generated regular MSC languages
• On recognizable subsets of free partially commutative monoids
• Realizability and verification of MSC graphs
• Reasoning about sequential and branching behaviours of message sequence graphs
• Safe realizability of high-level message sequence charts
• Synthesizing distributed finite-state systems from MSCs
• SYNTHESIZING STATE-BASED OBJECT SYSTEMS FROM LSC SPECIFICATIONS

Cited in

(25)

• Automated verification of automata communicating via FIFO and bag buffers
• Bounded MSC communication
• Compositional message sequence charts
• Shared-memory systems and charts
• The Synthesis Problem of Netcharts
• Realizability Criteria for Compositional MSC
• Safe realizability of high-level message sequence charts
• HMSCs as partial specifications . . . with PNs as completions
• From finite state communication protocols to high-level message sequence charts
• Realizability and verification of MSC graphs
• Synthesizing distributed finite-state systems from MSCs
• scientific article; zbMATH DE number 2086413 (Why is no real title available?)
• scientific article; zbMATH DE number 2086660 (Why is no real title available?)
• scientific article; zbMATH DE number 2087438 (Why is no real title available?)
• Dynamic communicating automata and branching high-level MSCs
• Fundamental Approaches to Software Engineering
• Synthesis of Safe Message-Passing Systems
• Tools and Algorithms for the Construction and Analysis of Systems
• High-level message sequence charts and projections.
• Comparing channel restrictions of communicating state machines, high-level message sequence charts, and multiparty session types
• Synthesis and Analysis of Petri Nets from Causal Specifications
• An automata-based approach for synchronizable mailbox communication
• An automata-based approach for synchronizable mailbox communication
• Certified implementability of global multiparty protocols
• Causal message sequence charts

This page was built for publication: Infinite-state high-level MSCs: model-checking and realizability

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