Formalizing operator task analysis

Human operators are unique in their decision making capability, judgment and nondeterminism. Their sense of judgment, unpredictable decision procedures, susceptibility to environmental elements can cause them to erroneously execute a given task description to operate a computer system. Usually, a computer system is protected against some erroneous human behaviors by having necessary safeguard mechanisms in place. But some erroneous human operator behaviors can lead to severe or even fatal consequences especially in safety critical systems. A generalized methodology that can allow modeling and analyzing the interactions between computer systems and human operators where the operators are allowed to deviate from their prescribed behaviors will provide a formal understanding of the robustness of a computer system against possible aberrant behaviors by its human operators. We provide several methodology for assisting in modeling and analyzing human behaviors exhibited while operating computer systems. Every human operator is usually given a specific recommended set of guidelines for operating a system. We first present process algebraic methodology for modeling and verifying recommended human task execution behavior. We present how one can perform runtime monitoring of a computer system being operated by a human operator for checking violation of temporal safety properties. We consider the concept of a protection envelope giving a wider class of behaviors than those strictly prescribed by a human task that can be tolerated by a system. We then provide a framework for determining whether a computer system can maintain its guarantees if the human operators operate within their protection envelopes. This framework also helps to determine the robustness of the computer system under weakening of the protection envelopes. In this regard, we present a tool called Tutela that assists in implementing the framework. We then examine the ability of a system to remain safe under broad classes of variations of the prescribed human task. We develop a framework for addressing two issues. The first issue is: given a human task specification and a protection envelope, will the protection envelope properties still hold under standard erroneous executions of that task by the human operators? In other words how robust is the protection envelope? The second issue is: in the absence of a protection envelope, can we approximate a protection envelope encompassing those standard erroneous human behaviors that can be safely endured by the system? We present an extension of Tutela that implements this framework. The two frameworks mentioned above use Concurrent Game Structures (CGS) as models for both computer systems and their human operators. However, there are some shortcomings of this formalism for our uses. We add incomplete information concepts in CGSs to achieve better modularity for the players. We introduce nondeterminism in both the transition system and strategies of players and in the modeling of human operators and computer systems. Nondeterministic action strategies for players in \emph{i}ncomplete information \emph{N}ondeterministic CGS (iNCGS) is a more precise formalism for modeling human behaviors exhibited while operating a computer system. We show how we can reason about a human behavior satisfying a guarantee by providing a semantics of Alternating Time Temporal Logic based on iNCGS player strategies. In a nutshell this dissertation provides formal methodology for modeling and analyzing system robustness against both expected and erroneous human operator behaviors.

Microcantilever sensors for biochemical detection and analysis

Biochemical agents, including bacteria and toxins, are potentially dangerous and responsible for a wide variety of diseases. Reliable detection and characterization of small samples is necessary in order to reduce and eliminate their harmful consequences. Microcantilever sensors offer a potential alternative to the state of the art due to their small size, fast response time, and the ability to operate in air and liquid environments. At present, there are several technology limitations that inhibit application of microcantilever to biochemical detection and analysis, including difficulties in conducting temperature-sensitive experiments, material inadequacy resulting in insufficient cell capture, and poor selectivity of multiple analytes. This work aims to address several of these issues by introducing microcantilevers having integrated thermal functionality and by introducing nanocrystalline diamond as new material for microcantilevers. Microcantilevers are designed, fabricated, characterized, and used for capture and detection of cells and bacteria. The first microcantilever type described in this work is a silicon cantilever having highly uniform in-plane temperature distribution. The goal is to have 100 μm square uniformly heated area that can be used for thermal characterization of films as well as to conduct chemical reactions with small amounts of material. Fabricated cantilevers can reach above 300C while maintaining temperature uniformity of 2−4%. This is an improvement of over one order of magnitude over currently available cantilevers. The second microcantilever type is a doped single crystal silicon cantilever having a thin coating of ultrananocrystalline diamond (UNCD). The primary application of such a device is in biological testing, where diamond acts as a stable, electrically isolated reaction surface while silicon layer provides controlled heating with minimum variations in temperature. This work shows that composite cantilevers of this kind are an effective platform for temperature-sensitive biological experiments, such as heat lysing and polymerase chain reaction. The rapid heat-transfer of Si-UNCD cantilever compromised the membrane of NIH 3T3 fibroblast and lysed the cell nucleus within 30 seconds. Bacteria cells, Listeria monocytogenes V7, were shown to be captured with biotinylated heat-shock protein on UNCD surface and 90% of all viable cells exhibit membrane porosity due to high heat in 15 seconds. Lastly, a sensor made solely from UNCD diamond is fabricated with the intention of being used to detect the presence of biological species by means of an integrated piezoresistor or through frequency change monitoring. Since UNCD diamond has not been previously used in piezoresistive applications, temperature-denpendent piezoresistive coefficients and gage factors are determined first. The doped UNCD exhibits a significant piezoresistive effect with gauge factor of 7.53±0.32 and a piezoresistive coefficient of 8.12×10^−12 Pa^−1 at room temperature. The piezoresistive properties of UNCD are constant over the temperature range of 25−200C. 300 μm long cantilevers have the highest sensitivity of 0.186 m-Ohm/Ohm per μm of cantilever end deflection, which is approximately half that of similarly sized silicon cantilevers. UNCD cantilever arrays were fabricated consisting of four sixteen-cantilever arrays of length 20–90 μm in addition to an eight-cantilever array of length 120 μm. Laser doppler vibrometry (LDV) measured the cantilever resonant frequency, which ranged as 218 kHz−5.14 MHz in air and 73 kHz−3.68 MHz in water. The quality factor of the cantilever was 47−151 in air and 18−45 in water. The ability to measure frequencies of the cantilever arrays opens the possibility for detection of individual bacteria by monitoring frequency shift after cell capture.