Automated Analysis of Probabilistic Open Systems

点击翻译按钮获取中文摘要

0098037Automated Analysis of Probabilistic Open SystemsS. Purushothaman IyerW. Rance Cleaveland (Co-PI)Concurrent systems such as network protocols and net-centric programsare difficult to build and debug because of the potential they exhibitfor unintended process interactions. The development of net-basedapplications which have to contend with probabilistic guarantees fromlower-levels is even more difficult as they need to be functionallycorrect and also satisfy reliability/performance constraints. Thisproject will investigate how formal methods can be extended to addressboth logical correctness and reliability/performance constraints.The current project will explore semantic theories of systems thathave both non-determinism and probabilistic choice. In particular,notions of equality and approximate equality of system behaviors willbe investigated. Furthermore, the effect of these notions oncompositional reasoning will also be studied.The second topic of the proposed work will be a thorough comparison ofthe semantic theories developed in this project against traditionalapproaches to dealing with non-determinism and probabilistic choice.Finally, practical algorithms for process minimization and forchecking equality (and approximate equality) of processes will bedesigned and implemented in the Concurrency Workbench of New Century.Case studies, to evaluate the proposed theories, will also beconstructed and studied.