Supervisory Control of Software Execution for Failure Avoidance: Experience from the Gadara Project

作     者：Yin Wang Hyoun Kyu Cho Hongwei Liao Ahmed Nazeem Terence P. Kelly Stéphane Lafortune Scott Mahlke Spyros A. Reveliotis 

作者机构：Hewlett-Packard Laboratories Department of Electrical engineering and Computer Science University of Michigan School of Industrial & Systems Engineering Georgia Institute of Technology 

出 版 物：《IFAC Proceedings Volumes》 

年 卷 期：2010年第43卷第12期

页      面：259-266页

主　　题：Discrete Event Systems Supervisory Control Petri Nets Software Failures Deadlock 

摘      要：We discuss our experience in the Gadara project, whose objective is to control the execution of software to avoid potential failures using discrete-event control techniques. We summarize our accomplishments so far and discuss future challenges. After initial work on safety of workflow scripts via supervisory control techniques, we have focused our efforts on deadlock avoidance in multithreaded C programs that use locking primitives to control access to shared data. We describe how we automatically construct automata models of workflows and Petri net models of concurrent programs. In the case of multithreaded C programs, the resulting models characterize a new class of resource-allocation Petri nets called Gadara nets. These nets enjoy structural properties that facilitate the synthesis of liveness-enforcing control policies that are maximally-permissive. We describe our strategy for run-time implementation of these control policies, especially by a technique known as code instrumentation. It is hoped that the lessons learned so far in the Gadara project will be useful in other application areas and will suggest avenues for future theoretical investigations.