首页> 外文学位 >Software failure avoidance using discrete control theory.
【24h】

Software failure avoidance using discrete control theory.

机译:使用离散控制理论避免软件故障。

获取原文
获取原文并翻译 | 示例

摘要

Software reliability is an increasingly pressing concern as the multicore revolution forces parallel programming upon the average programmer. Many existing approaches to software failure are ad hoc, based on best-practice heuristics. Often these approaches impose onerous burdens on developers, entail high runtime performance overheads, or offer no help for unmodified legacy code. We demonstrate that discrete control theory can be applied to software failure avoidance problems.;Discrete control theory is a branch of control engineering that addresses the control of systems with discrete state spaces and event-driven dynamics. Typical modeling formalisms used in discrete control theory include automata and Petri nets, which are well suited for modeling software systems. In order to use discrete control theory for software failure avoidance problems, formal models of computer programs must first be constructed. Next, control logic must be synthesized from the model and given behavioral specifications. Finally, the control logic must be embedded into the execution engine or the program itself. At runtime, the provably correct control logic guarantees that the given failure-avoidance specifications are enforced.;This thesis employs the above methodology in two different application domains: failure avoidance in information technology automation workflows and deadlock avoidance in multithreaded C programs. In the first application, we model workflows using finite-state automata and synthesize controllers for safety and nonblocking specifications expressed as regular languages using an automata-based discrete control technique, called Supervisory Control. The second application addresses the problem of deadlock avoidance in multithreaded C programs that use lock primitives. We exploit compiler technology to model programs as Petri nets and establish a correspondence between deadlock avoidance in the program and the absence of reachable empty siphons in its Petri net model. The technique of Supervision Based on Place Invariants is then used to synthesize the desired control logic, which is implemented using source-to-source translation.;Empirical evidence confirms that the algorithmic techniques of Discrete Control Theory employed scale to programs of practical size in both application domains. Furthermore, comprehensive experiments in the deadlock avoidance problem demonstrate tolerable runtime overhead, no more than 18%, for a benchmark and several real-world C programs.
机译:随着多核革命迫使普通编程人员进行并行编程,软件可靠性日益受到关注。基于最佳实践启发式方法,许多现有的解决软件故障的方法都是临时的。通常,这些方法给开发人员带来了沉重的负担,带来了较高的运行时性能开销,或者对未修改的旧代码没有帮助。我们证明了离散控制理论可以应用于软件故障避免问题。离散控制理论是控制工程的一个分支,致力于解决具有离散状态空间和事件驱动动力学的系统的控制问题。离散控制理论中使用的典型建模形式包括自动机和Petri网,它们非常适合对软件系统进行建模。为了将离散控制理论用于避免软件故障的问题,必须首先构建计算机程序的正式模型。接下来,必须从模型和给定的行为规范中综合控制逻辑。最后,控制逻辑必须嵌入执行引擎或程序本身。在运行时,可证明正确的控制逻辑可确保强制执行给定的避免故障规范。;本文在两个不同的应用领域中采用了上述方法:信息技术自动化工作流中的故障避免和多线程C程序中的死锁避免。在第一个应用程序中,我们使用有限状态自动机对工作流进行建模,并使用基于自动机的离散控制技术(称为监督控制),将安全性和无阻塞规范合成为规则语言,以表达安全性和非阻塞性规范。第二个应用程序解决了使用锁定原语的多线程C程序中避免死锁的问题。我们利用编译器技术将程序建模为Petri网,并在程序中避免死锁和在其Petri网模型中没有可到达的空虹吸管之间建立对应关系。然后使用基于位置不变性的监督技术来合成所需的控制逻辑,该控制逻辑通过使用源到源转换来实现。应用程序域。此外,针对避免死锁问题的综合实验表明,对于基准测试和一些实际的C程序,可忍受的运行时开销(不超过18%)。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱:kefu@zhangqiaokeyan.com

京公网安备:11010802029741号 ICP备案号:京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有
  • 客服微信

  • 服务号