Abstract A safety verification task involves verifying a system against a desired safety property under certain assumptions about the environment. However, these environmental assumptions may occasionally be violated due to modeling errors or faults. Ideally, the system guarantees its critical properties even under some of these violations, i.e., the system is robust against environmental deviations. This paper proposes a notion of robustness as an explicit, first-class property of a transition system that captures how robust it is against possible deviations in the environment. We modeled deviations as a set of transitions that may be added to the original environment. Our robustness notion then describes the safety envelope of this system, i.e., it captures all sets of extra environment transitions for which the system still guarantees a desired property. We show that being able to explicitly reason about robustness enables new types of system analysis and design tasks beyond the common verification problem stated above. We demonstrate the application of our framework on case studies involving a radiation therapy interface, an electronic voting machine, a fare collection protocol, and a medical pump device.

System development often involves decisions about how a high-level design is to be implemented using primitives from a low-level platform. Certain decisions, however, may introduce undesirable behavior into the resulting implementation, possibly leading to a violation of a desired property that has already been established at the design level. In this paper, we introduce the problem of synthesizing a property-preserving platform mapping: synthesize a set of implementation decisions ensuring that a desired property is preserved from a high-level design into a low-level platform implementation. We formalize this synthesis problem and propose a technique for generating a mapping based on symbolic constraint search. We describe our prototype implementation, and two real-world case studies demonstrating the applicability of our technique to the synthesis of secure mappings for the popular web authorization protocols OAuth 1.0 and 2.0.

In the multicore era, developers face increasing pressure to parallelize their programs. However, building correct and efficient concurrent programs is substantially more difficult than building sequential ones. To address the multicore challenge, numerous tools have been developed to assist multithreaded programmers, including static and dynamic bug detectors, automated bug fixers, and optimization tools. Many of these tools rely on or benefit from the precise identification of critical sections, i.e., sections where the thread of execution holds at least one lock. For languages where critical sections are not lexically scoped, e.g., C/C++, static analysis often fails to pair up lock and unlock calls correctly. In this paper, we propose a practical lock/unlock pairing mechanism that combines static analysis with dynamic instrumentation to identify critical sections in POSIX multithreaded C/C++ programs. Our method first applies a con-servative inter-procedural path-sensitive dataflow analysis to pair up all lock and unlock calls. When the static analysis fails, our method makes assumptions about the pairing using common heuristics. These assumptions are checked at runtime using lightweight instrumentation. Our experiments show that only one out of 891 lock/unlock pairs violates our assumptions at runtime and the instrumentation imposes negligible overhead of 3.34% at most, for large open-source server programs. Overall, our mechanism can pair up 98.2% of all locks including 7.1 % of them paired speculatively.

Our objective is to develop a general and versatile approach for building structured formal models of complex automated systems in order to facilitate their control and diagnosis. For this purpose, we present a methodology that builds the complete model of a system by composing models of the individual hardware components, their physical coupling, and the associated control logic. We choose to employ a hierarchical decomposition that separates the control logic into a high level that manages the sequence of control actions and a low level that implements the control actions. The low level is composed of control logic and physical components (sensors and actuators) grouped into a device. In order to capture the physical constraints between the components in a device, we propose the notion of a physical constraint automaton, which is composed with the generic component automata to generate the complete model of the device. We also show how the methodology allows the introduction of component faults into the overall model. The effectiveness of the proposed approach is demonstrated on a micro flexible manufacturing system.

Deadlock in multithreaded programs is an increasingly important problem as ubiquitous multicore architectures force parallelization upon an ever wider range of software. This paper presents a theoretical foundation for dynamic deadlock avoidance in concurrent programs that employ conventional mutual exclusion and synchronization primitives (e.g., multithreaded C/Pthreads programs). Beginning with control flow graphs extracted from program source code, we construct a formal model of the program and then apply Discrete Control Theory to automatically synthesize deadlock-avoidance control logic that is implemented by program instrumentation. At run time, the control logic avoids deadlocks by postponing lock acquisitions. Discrete Control Theory guarantees that the program instrumented with our synthesized control logic cannot deadlock. Our method furthermore guarantees that the control logic is maximally permissive: it postpones lock acquisitions only when necessary to prevent deadlocks, and therefore permits maximal runtime concurrency. Our prototype for C/Pthreads scales to real software including Apache, OpenLDAP, and two kinds of benchmarks, automatically avoiding both injected and naturally occurring deadlocks while imposing modest runtime overheads.

As information technology (IT) administration becomes increasingly complex, workflow technologies are gaining popularity for IT automation. Writing correct workflow programs is notoriously difficult. Although static analysis tools are available, fixing defects remains manual and error-prone. This paper applies discrete control theory to IT automation workflows. Discrete control detects flaws in workflows just as static analysis does, and more importantly it also allows safe execution of flawed workflows by dynamically avoiding run-time failures. Our approach can guarantee compliance with certain requirements and can partially decouple requirements from software, reducing the need to modify the latter if the former change. We have implemented a discrete control module for a real IT automation system. Experiments with workflows from a real production system and with randomly generated workflows show that our approach scales to workflows of practical size.

This paper studies online fault detection and isolation of modular dynamic systems modeled as sets of place-bordered Petri nets. The common places among the set of Petri nets modeling a system capture coupling of various system components. The transitions are labeled by events, some of which are unobservable (i.e., not directly recorded by the sensors attached to the system). The events whose occurrence must be diagnosed have unobservable transition labels. These events model faults or other significant changes in the system state. The existing theory of diagnosis of discrete-event systems is extended in the context of the above model. The modular structure of the system is exploited by a distributed algorithm for fault diagnosis. A Petri net diagnoser is associated with every Petri net and the diagnosers communicate in real time during the diagnostic process when the token count of common places changes. A merge function is defined to combine the individual diagnoser states and recover the complete diagnoser state that would be obtained under a monolithic approach. Strategies that reduce the communication overhead are presented. The software implementation of the distributed algorithm is discussed. Note to Practitioners-In the last decade, monitoring, fault detection, and diagnosis methodologies based on the use of discrete-event models have been successfully used in a variety of technological systems ranging from document processing systems to intelligent transportation systems. This paper was motivated by the problem of fault diagnosis for modular (distributed) dynamic discrete-event systems (DES). As a DES modeling formalism, Petri nets offer potential advantages in terms of the distributed representation of the system and the ability to represent coupling of the system components. The systems studied in this paper are sets of modules coupled with each other through various system components and modeled using Petri nets. We present a distributed fault diagnosis algorithm which allows each module in the distributed system to diagnose its faults independently unless completion of a task requires the use of coupled components. In the case of coupling, modules communicate with each other to accurately diagnose the fault. The distributed fault diagnosis algorithm recovers the monolithic diagnosis information at the cost of communication and growing communication overhead. To mitigate that problem, we present an improved version of the algorithm that significantly reduces the communication overhead. Finally, we introduce the software toolbox (written in Matlab and integrated with AT&T Graphviz) and we present a case study of an example of a heating, ventilation, and air-conditioning system where we use the software tool for modeling and analyzing the system

This paper presents a variation of the methodology, established in a previous paper, to test a modular system for nonconflict using abstractions of its supervisors. In this work, information about the model and control structure of the system are used to derive a solution where some of the conditions established before are not required. The local modular approach is used to design the supervisors and supervisor reduction techniques are also used to help defining the set of events that are kept in the abstractions.

The decentralized control problem that we address in this paper is that of several communicating supervisory controllers, each with different information, working in concert to exactly achieve a given legal sublanguage of the uncontrolled system's language model. We present a novel information structure formalism for dealing with this class of problems. Preliminary results are presented which elucidate a fundamental concept in decentralized control problems: the importance of controllers anticipating future possible communications.

We address the problem of failure diagnosis in discrete event systems with decentralized information. We propose a coordinated decentralized architecture consisting of local sites communicating with a coordinator that is responsible for diagnosing the failures occurring in the system. We extend the notion of diagnosability, originally introduced in Sampath et al. (1995) for centralized systems, to the proposed coordinated decentralized architecture. We specify three protocols, i.e. the diagnostic information generated at the local sites, the communication rules used by the local sites, and the coordinator's decision rule, that realize the proposed architecture. We analyze the diagnostic properties of each protocol. We also state and prove necessary and sufficient conditions for a language to be diagnosable under each protocol. These conditions are checkable off-line. The online diagnostic process is carried out using the diagnosers introduced in the above article or a slight variation of these diagnosers. The key features of the proposed protocols are: (i) they achieve, each under a set of assumptions, the same diagnostic performance as the centralized diagnoser; and (ii) they highlight the performance vs. complexity tradeoff that arises in coordinated decentralized architectures. The correctness of two of the protocols relies on some stringent global ordering assumptions on message reception at the coordinator's site, the relaxation of which is briefly discussed.

This paper deals with a new type of optimal control for discrete event systems that extends the theory of Sengupta and Lafortune (1998). Our aim is to make a system optimally evolve through a set of multiple goals, one by one, with no order necessarily prespecified. Our method is divided into two steps. We first use the earlier results to synthesize individual optimal controllers for each goal. We then develop the solution of another optimal control problem, namely, how to adapt, if necessary, and schedule all of the controllers built in the first step in order to visit all of the goals with least total cost. We solve this problem by defining the notion of a scheduler and then by mapping the problem of finding an optimal scheduler to an instance of the traveling salesman problem.

Article An information model for genome map representation and assembly Share on Authors: A. J. Lee Department of EECS, University of Michigan, Ann Arbor, Ann Arbor, MI Department of EECS, University of Michigan, Ann Arbor, Ann Arbor, MIView Profile , E. A. Rendensteiner Department of EECS, University of Michigan, Ann Arbor, Ann Arbor, MI Department of EECS, University of Michigan, Ann Arbor, Ann Arbor, MIView Profile , S. Thomas Information Technology and Networking, University of Michigan Medical Center, Human Genome Center, 2570C MSRB II Information Technology and Networking, University of Michigan Medical Center, Human Genome Center, 2570C MSRB IIView Profile , S. Lafortune Department of EECS, University of Michigan, Ann Arbor, Ann Arbor, MI Department of EECS, University of Michigan, Ann Arbor, Ann Arbor, MIView Profile Authors Info & Claims CIKM '93: Proceedings of the second international conference on Information and knowledge managementDecember 1993 Pages 75–84https://doi.org/10.1145/170088.170107Published:01 December 1993 5citation1,221DownloadsMetricsTotal Citations5Total Downloads1,221Last 12 Months0Last 6 weeks0 Get Citation AlertsNew Citation Alert added!This alert has been successfully added and will be sent to:You will be notified whenever a record that you have chosen has been cited.To manage your alert preferences, click on the button below.Manage my AlertsNew Citation Alert!Please log in to your account Save to BinderSave to BinderCreate a New BinderNameCancelCreateExport CitationPublisher SiteGet Access

The problem of finding an optimal semijoin sequence that fully reduces a given tree query is discussed. A method is presented that intelligently navigates the space of all semijoin sequences and returns an optimal solution. Experiments are reported that show that this method performs very efficiently: on average, less than 5% of the search space is searched before an optimal solution is found. Other advantages of the method are ease of implementation, generality of the cost mode considered, and ability to handle tree queries with arbitrary target lists.>

A state transition model for the optimization of query processing in a distributed database system is presented. The problem is parameterized by means of a state describing the amount of processing that has been performed at each site where the database is located. A state transition occurs each time a new join or semijoin is executed. Dynamic programming is used to compute recursively the costs of the states and the globally optimal solution, taking into account communication and local processing costs. The state transition model is general enough to account for the possibility of parallel processing among the various sites, as well as for redundancy in the database. The model also permits significant reductions of the necessary computations by taking advantage of simple additivity and site-uniformity properties of a cost model, and of clever strategies that improve on the basic dynamic programming algorithm.