Verification of Well-formedness in Message-Passing Asynchronous Systems modeled as Communicating Finite-State Machines

Date
2017-01-01
Authors
Nalla, Shiva
Journal Title
Journal ISSN
Volume Title
Publisher
Source URI
Altmetrics
Authors
Research Projects
Organizational Units
Computer Science
Organizational Unit
Journal Issue
Series
Abstract

Asynchronous systems with message-passing communication paradigm have made major inroads in many application domains in service-oriented computing, secure and safe operating systems and in general, distributed systems. Asynchrony and concurrency in these systems bring in new challenges in verification of correctness properties. In particular, the high-level behavior of message-passing asynchronous systems is modeled as communicating finite-state machines (CFSMs) with unbounded communication buffers/channels. It has been proven that, in general, state-space exploration based automatic verification of CFSMs is undecidable - specifically, reachability and boundedness problems for CFSMs are undecidable. In this context, we focus on an important path-based property for CFSMs, namely well-formedness - every message sent can be eventually consumed. We show that well-formedness is undecidable as well, and present decidable sub-classes for which verification of well-formedness can be automated. We implemented the algorithm for verifying the well-formedness for the decidable subclass, and present our results using several case studies such as service choreographies and Singularity OS contracts.

Description
Keywords
Asynchronous systems, automatic verification, boundedness, synchronizability, undecidability, well-formedness
Citation