Modern web applications combine persistent state updates, concurrent interactions, and unreliable communication with external services. Failures such as timeouts can occur after partial state changes, producing temporary inconsistencies whose resolution depends on liveness properties that are often not verified in practice. Although formal methods offer rigorous guarantees for reasoning about complex software, they remain rarely adopted in enterprise settings due to their perceived complexity and lack of practical automation. Multiparty Session Types (MPST) offer strong guarantees for communication safety, yet they do not account for the interplay between state evolution, dynamic workflow structure, and failure behaviour that are essential for reasoning about the correctness of real web applications. This paper introduces a global-type framework that equips MPST with explicit failure semantics and dynamic participation. We define the syntax and operational semantics of these enriched global types and establish core properties, including coherence preservation. This foundation enables formal reasoning about communications in web applications where failures may occur, and lays the groundwork for future stateful extensions and automated verification of liveness properties.

翻译：现代Web应用结合了持久状态更新、并发交互以及与外部服务的不可靠通信。超时等故障可能在部分状态变更后发生，产生临时不一致性，其解析依赖于实践中常未验证的活性属性。尽管形式化方法为复杂软件的推理提供了严格保证，但由于其感知复杂性及缺乏实用自动化，在企业环境中仍鲜少采用。多方会话类型（MPST）为通信安全性提供了强保证，但未考虑状态演化、动态工作流结构及故障行为之间的相互作用——而这些对于推理真实Web应用的正确性至关重要。本文引入一种全局类型框架，为MPST配备显式故障语义与动态参与机制。我们定义了这些增强全局类型的语法与操作语义，并建立了核心性质（包括一致性保持）。该基础使得对可能发生故障的Web应用中的通信进行形式化推理成为可能，并为未来有状态扩展及活性属性的自动验证奠定了基础。