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

dc.contributor.advisor Samik Basu Nalla, Shiva
dc.contributor.department Computer Science 2018-08-11T08:34:46.000 2020-06-30T03:03:32Z 2020-06-30T03:03:32Z Sun Jan 01 00:00:00 UTC 2017 2001-01-01 2017-01-01
dc.description.abstract <p>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.</p>
dc.format.mimetype application/pdf
dc.identifier archive/
dc.identifier.articleid 6394
dc.identifier.contextkey 11051454
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath etd/15387
dc.language.iso en
dc.source.bitstream archive/|||Fri Jan 14 20:40:05 UTC 2022
dc.subject.disciplines Computer Sciences
dc.subject.keywords Asynchronous systems
dc.subject.keywords automatic verification
dc.subject.keywords boundedness
dc.subject.keywords synchronizability
dc.subject.keywords undecidability
dc.subject.keywords well-formedness
dc.title Verification of Well-formedness in Message-Passing Asynchronous Systems modeled as Communicating Finite-State Machines
dc.type article
dc.type.genre thesis
dspace.entity.type Publication
relation.isOrgUnitOfPublication f7be4eb9-d1d0-4081-859b-b15cee251456 Computer Science thesis Master of Science
Original bundle
Now showing 1 - 1 of 1
758.9 KB
Adobe Portable Document Format