Automated Analysis of Probabilistic Open Systems

North Carolina State University, Raleigh NC

Investigators

Abstract

0098037 Automated Analysis of Probabilistic Open Systems S. Purushothaman Iyer W. Rance Cleaveland (Co-PI) Concurrent systems such as network protocols and net-centric programs are difficult to build and debug because of the potential they exhibit for unintended process interactions. The development of net-based applications which have to contend with probabilistic guarantees from lower-levels is even more difficult as they need to be functionally correct and also satisfy reliability/performance constraints. This project will investigate how formal methods can be extended to address both logical correctness and reliability/performance constraints. The current project will explore semantic theories of systems that have both non-determinism and probabilistic choice. In particular, notions of equality and approximate equality of system behaviors will be investigated. Furthermore, the effect of these notions on compositional reasoning will also be studied. The second topic of the proposed work will be a thorough comparison of the semantic theories developed in this project against traditional approaches to dealing with non-determinism and probabilistic choice. Finally, practical algorithms for process minimization and for checking equality (and approximate equality) of processes will be designed and implemented in the Concurrency Workbench of New Century. Case studies, to evaluate the proposed theories, will also be constructed and studied.