Podorozhny, RodionMcDermott, Mark2021-05-102021-05-102021-08McDermott, M. (2021). <i>Rigorous analysis Of combined software processes via model checking</i> (Unpublished thesis). Texas State University, San Marcos, Texas.https://hdl.handle.net/10877/13515The 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.Text117 pages1 file (.pdf)enSoftwareProcessesConcurrencyThesis