Rigorous Analysis Of Combined Software Processes Via Model Checking
Date
2021-08
Authors
McDermott, Mark
Journal Title
Journal ISSN
Volume Title
Publisher
Abstract
The ability to automatically combine and analyze multiple concurrent processes, perhaps written by different people, becomes increasingly important in the modern mobile, distributed, and ad-hoc computational environments. For instance, medical processes that guide medical procedures in hospitals are written by different people, yet they are performed concurrently on the same patient. There are critical properties that such combined, concurrent processes must adhere to. Failure to adhere to such properties may result in the loss of life or serious disability. This work presents an automatic verification system written from scratch (about 32,000 lines of Java) that takes in
rigorous descriptions of individual processes in Little-JIL, translates them semantically, combines them into an ad-hoc concurrent process, and performs static verification against specified critical properties via CTL model checking algorithms.
Description
Keywords
Software, Processes, Concurrency
Citation
McDermott, M. (2021). <i>Rigorous analysis Of combined software processes via model checking</i> (Unpublished thesis). Texas State University, San Marcos, Texas.