Automated Analysis of Probabilistic Open Systems

概率开放系统的自动分析

• 批准号: 0098037
• 负责人: S. Iyer
• 金额: $ 21万
• 依托单位: North Carolina State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2001
• 资助国家: 美国
• 起止时间: 2001-09-15 至 2005-07-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0098037&HistoricalAwards=false
• 关键词: Automated; Analysis; 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.

0098037概率开放系统自动分析。Purushothaman IyerW.Rance Cleaveland(Co-PI)并发系统(如网络协议和以网络为中心的程序)很难构建和调试，因为它们可能会出现意外的进程交互。开发必须与来自低层的概率保证作斗争的基于网络的应用程序更加困难，因为它们需要在功能上是正确的，并满足可靠性/性能约束。这个项目将研究如何将形式化方法扩展到处理逻辑正确性和可靠性/性能约束。当前项目将探索具有非确定性和概率选择的系统的语义理论。特别是，系统行为的相等性和近似相等性的概念将被研究。第二个主题将是将本项目中发展的语义理论与传统的处理非确定性和概率选择的方法进行深入的比较。最后，将在新世纪的并发工作台上设计和实现实用的进程最小化和进程的等价性(和近似等价性)检查算法。