Automated Analysis of Probabilistic Open Systems

概率开放系统的自动化分析[j]。公司IyerW Purushothaman。像网络协议和以网络为中心的程序这样的并发系统很难构建和调试，因为它们可能会显示出意想不到的进程交互。基于网络的应用程序的开发必须与来自底层的概率保证相抗衡，这更加困难，因为它们需要功能正确并满足可靠性/性能约束。该项目将研究如何扩展形式化方法以解决逻辑正确性和可靠性/性能约束。目前的项目将探索具有非决定论和概率选择的系统的语义理论。特别地，系统行为的相等和近似相等的概念将被研究。此外，这些概念对组合推理的影响也将被研究。本研究的第二个主题是将本研究中发展的语义理论与处理非确定性和概率选择的传统方法进行全面比较。最后，在新世纪并发工作台中设计并实现了进程最小化和进程相等（近似相等）校验的实用算法。案例研究，以评估所提出的理论，也将被构建和研究。

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.