Verification of programs with half-duplex communication

DOI10.1016/j.ic.2005.05.006zbMath1101.68676OpenAlexW2040008220MaRDI QIDQ2573635

Alain Finkel, Gérard Cécé

Publication date: 22 November 2005

Published in: Information and Computation (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.ic.2005.05.006

zbMATH Keywords

DecidabilityPLTL model-checkingCommunicating finite state machinesChannel-recognizable reachability setsCTL model-checkingHalf-duplex communicationRegular model checkingSymbolic verification

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (22)

Relating two automata-based models of orchestration and choreography ⋮ Synchronizability for Verification of Asynchronously Communicating Systems ⋮ Compliance in Behavioural Contracts: A Brief Survey ⋮ Automated verification of automata communicating via FIFO and bag buffers ⋮ On deciding synchronizability for asynchronously communicating systems ⋮ Composition of synchronous communicating systems ⋮ Multiparty half-duplex systems and synchronous communications ⋮ On Composing Communicating Systems ⋮ On the boundary between decidability and undecidability of asynchronous session subtyping ⋮ Honesty by Typing ⋮ Unnamed Item ⋮ Unnamed Item ⋮ On the Undecidability of Asynchronous Session Subtyping ⋮ Unnamed Item ⋮ Verification of Flat FIFO Systems ⋮ An abstract framework for choreographic testing ⋮ Realisability of pomsets ⋮ Connecting open systems of communicating finite state machines ⋮ Unnamed Item ⋮ Non axiomatisability of positive relation algebras with constants, via graph homomorphisms ⋮ Unnamed Item ⋮ Unnamed Item

Uses Software

• TREX
• FAST
• LASH

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Undecidable verification problems for programs with unreliable channels
• Testing for unboundedness of fifo channels
• Reduction and covering of infinite reachability trees
• Verifying identical communicating processes is undecidable
• Well-abstracted transition systems: Application to FIFO automata.
• Verifying lossy channel systems has nonprimitive recursive complexity.
• Using forward reachability analysis for verification of lossy channel systems
• Unreliable channels are easier to verify than perfect channels
• Verifying programs with unreliable channels
• Symbolic reachability analysis of FIFO-channel systems with nonregular sets of configurations
• On Communicating Finite-State Machines
• On the progress of communication between two finite state machines

This page was built for publication: Verification of programs with half-duplex communication