SHF: Small: Static and Dynamic Techniques for Correctness of Probabilistic Systems

SHF：小：概率系统正确性的静态和动态技术

• 批准号: 1319754
• 负责人: Aravinda Sistla
• 金额: $ 30万
• 依托单位: University of Illinois at Chicago
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2013
• 资助国家: 美国
• 起止时间: 2013-09-01 至 2017-08-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1319754&HistoricalAwards=false
• 关键词: SHF; Small; Static; Dynamic; Techniques

Computerized systems are ubiquitous in modern society. They are present in our homes, cars, medical devices and various appliances. It is extremely important to ensure that these systems function without failing and work as they are intended to. This project explores basic research to ensure the correct functioning of such systems. The proposed research will contribute towards development of error free and high quality computerized systems, especially safety critical systems. It will also make it more difficult to break into systems, thus making them safer. It will lead to reduced down time of computer systems, thus yielding economic benefits as well. This project addresses fundamental research on static as well as dynamic techniques for ensuring correct functioning of probabilistic computer systems. The project proposes novel research on model checking concurrent probabilistic programs that exhibit individual process level non-determinism. It investigates model checking of such systems under different classes of schedulers that more accurately represent the resolution of non-determinism in them. The project also proposes dynamic techniques, based on monitoring, for ensuring correctness of probabilistic systems at run time when their internal state is not directly observable. Techniques based on state estimation are proposed and will be analyzed to ensure timely detection of malfunctioning.

计算机化系统在现代社会中无处不在。它们存在于我们的家中、汽车、医疗设备和各种电器中。确保这些系统正常运作并按预期发挥作用极为重要。该项目探索基础研究，以确保这些系统的正确运作。拟议的研究将有助于无差错和高质量的计算机系统，特别是安全关键系统的发展。这也将使入侵系统变得更加困难，从而使系统更加安全。这将导致减少计算机系统的停机时间，从而产生经济效益。该项目致力于静态和动态技术的基础研究，以确保概率计算机系统的正确运行。该项目提出了新的研究模型检查并发概率程序，表现出个人进程级的非确定性。它研究了模型检查的系统下，更准确地表示在他们的非确定性的决议不同类别的决策者。该项目还提出了动态技术，基于监测，以确保正确性的概率系统在运行时，其内部状态是不能直接观察。提出了基于状态估计的技术，并将进行分析，以确保及时检测故障。