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

dc.contributor.advisor Samik Basu
dc.contributor.author Nalla, Shiva
dc.contributor.department Computer Science
dc.date 2018-08-11T08:34:46.000
dc.date.accessioned 2020-06-30T03:03:32Z
dc.date.available 2020-06-30T03:03:32Z
dc.date.copyright Sun Jan 01 00:00:00 UTC 2017
dc.date.embargo 2001-01-01
dc.date.issued 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/lib.dr.iastate.edu/etd/15387/
dc.identifier.articleid 6394
dc.identifier.contextkey 11051454
dc.identifier.doi https://doi.org/10.31274/etd-180810-5011
dc.identifier.s3bucket isulib-bepress-aws-west
dc.identifier.submissionpath etd/15387
dc.identifier.uri https://dr.lib.iastate.edu/handle/20.500.12876/29570
dc.language.iso en
dc.source.bitstream archive/lib.dr.iastate.edu/etd/15387/Nalla_iastate_0097M_16289.pdf|||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
thesis.degree.discipline Computer Science
thesis.degree.level thesis
thesis.degree.name Master of Science
File
Original bundle
Now showing 1 - 1 of 1
Name:
Nalla_iastate_0097M_16289.pdf
Size:
758.9 KB
Format:
Adobe Portable Document Format
Description: