On-Chip Thermal Monitoring: Design, Placement and Interconnection of Temperature Sensors

La temperatura es una preocupación que juega un papel protagonista en el diseño de circuitos integrados modernos. El importante aumento de las densidades de potencia que conllevan las últimas generaciones tecnológicas ha producido la aparición de gradientes térmicos y puntos calientes durante el funcionamiento normal de los chips. La temperatura tiene un impacto negativo en varios parámetros del circuito integrado como el retardo de las puertas, los gastos de disipación de calor, la fiabilidad, el consumo de energía, etc. Con el fin de luchar contra estos efectos nocivos, la técnicas de gestión dinámica de la temperatura (DTM) adaptan el comportamiento del chip en función en la información que proporciona un sistema de monitorización que mide en tiempo de ejecución la información térmica de la superficie del dado. El campo de la monitorización de la temperatura en el chip ha llamado la atención de la comunidad científica en los últimos años y es el objeto de estudio de esta tesis. Esta tesis aborda la temática de control de la temperatura en el chip desde diferentes perspectivas y niveles, ofreciendo soluciones a algunos de los temas más importantes. Los niveles físico y circuital se cubren con el diseño y la caracterización de dos nuevos sensores de temperatura especialmente diseñados para los propósitos de las técnicas DTM. El primer sensor está basado en un mecanismo que obtiene un pulso de anchura variable dependiente de la relación de las corrientes de fuga con la temperatura. De manera resumida, se carga un nodo del circuito y posteriormente se deja flotando de tal manera que se descarga a través de las corrientes de fugas de un transistor; el tiempo de descarga del nodo es la anchura del pulso. Dado que la anchura del pulso muestra una dependencia exponencial con la temperatura, la conversión a una palabra digital se realiza por medio de un contador logarítmico que realiza tanto la conversión tiempo a digital como la linealización de la salida. La estructura resultante de esta combinación de elementos se implementa en una tecnología de 0,35 _m. El sensor ocupa un área muy reducida, 10.250 nm2, y consume muy poca energía, 1.05-65.5nW a 5 muestras/s, estas cifras superaron todos los trabajos previos en el momento en que se publicó por primera vez y en el momento de la publicación de esta tesis, superan a todas las implementaciones anteriores fabricadas en el mismo nodo tecnológico. En cuanto a la precisión, el sensor ofrece una buena linealidad, incluso sin calibrar; se obtiene un error 3_ de 1,97oC, adecuado para tratar con las aplicaciones de DTM. Como se ha explicado, el sensor es completamente compatible con los procesos de fabricación CMOS, este hecho, junto con sus valores reducidos de área y consumo, lo hacen especialmente adecuado para la integración en un sistema de monitorización de DTM con un conjunto de monitores empotrados distribuidos a través del chip. Las crecientes incertidumbres de proceso asociadas a los últimos nodos tecnológicos comprometen las características de linealidad de nuestra primera propuesta de sensor. Con el objetivo de superar estos problemas, proponemos una nueva técnica para obtener la temperatura. La nueva técnica también está basada en las dependencias térmicas de las corrientes de fuga que se utilizan para descargar un nodo flotante. La novedad es que ahora la medida viene dada por el cociente de dos medidas diferentes, en una de las cuales se altera una característica del transistor de descarga |la tensión de puerta. Este cociente resulta ser muy robusto frente a variaciones de proceso y, además, la linealidad obtenida cumple ampliamente los requisitos impuestos por las políticas DTM |error 3_ de 1,17oC considerando variaciones del proceso y calibrando en dos puntos. La implementación de la parte sensora de esta nueva técnica implica varias consideraciones de diseño, tales como la generación de una referencia de tensión independiente de variaciones de proceso, que se analizan en profundidad en la tesis. Para la conversión tiempo-a-digital, se emplea la misma estructura de digitalización que en el primer sensor. Para la implementación física de la parte de digitalización, se ha construido una biblioteca de células estándar completamente nueva orientada a la reducción de área y consumo. El sensor resultante de la unión de todos los bloques se caracteriza por una energía por muestra ultra baja (48-640 pJ) y un área diminuta de 0,0016 mm2, esta cifra mejora todos los trabajos previos. Para probar esta afirmación, se realiza una comparación exhaustiva con más de 40 propuestas de sensores en la literatura científica. Subiendo el nivel de abstracción al sistema, la tercera contribución se centra en el modelado de un sistema de monitorización que consiste de un conjunto de sensores distribuidos por la superficie del chip. Todos los trabajos anteriores de la literatura tienen como objetivo maximizar la precisión del sistema con el mínimo número de monitores. Como novedad, en nuestra propuesta se introducen nuevos parámetros de calidad aparte del número de sensores, también se considera el consumo de energía, la frecuencia de muestreo, los costes de interconexión y la posibilidad de elegir diferentes tipos de monitores. El modelo se introduce en un algoritmo de recocido simulado que recibe la información térmica de un sistema, sus propiedades físicas, limitaciones de área, potencia e interconexión y una colección de tipos de monitor; el algoritmo proporciona el tipo seleccionado de monitor, el número de monitores, su posición y la velocidad de muestreo _optima. Para probar la validez del algoritmo, se presentan varios casos de estudio para el procesador Alpha 21364 considerando distintas restricciones. En comparación con otros trabajos previos en la literatura, el modelo que aquí se presenta es el más completo. Finalmente, la última contribución se dirige al nivel de red, partiendo de un conjunto de monitores de temperatura de posiciones conocidas, nos concentramos en resolver el problema de la conexión de los sensores de una forma eficiente en área y consumo. Nuestra primera propuesta en este campo es la introducción de un nuevo nivel en la jerarquía de interconexión, el nivel de trillado (o threshing en inglés), entre los monitores y los buses tradicionales de periféricos. En este nuevo nivel se aplica selectividad de datos para reducir la cantidad de información que se envía al controlador central. La idea detrás de este nuevo nivel es que en este tipo de redes la mayoría de los datos es inútil, porque desde el punto de vista del controlador sólo una pequeña cantidad de datos |normalmente sólo los valores extremos| es de interés. Para cubrir el nuevo nivel, proponemos una red de monitorización mono-conexión que se basa en un esquema de señalización en el dominio de tiempo. Este esquema reduce significativamente tanto la actividad de conmutación sobre la conexión como el consumo de energía de la red. Otra ventaja de este esquema es que los datos de los monitores llegan directamente ordenados al controlador. Si este tipo de señalización se aplica a sensores que realizan conversión tiempo-a-digital, se puede obtener compartición de recursos de digitalización tanto en tiempo como en espacio, lo que supone un importante ahorro de área y consumo. Finalmente, se presentan dos prototipos de sistemas de monitorización completos que de manera significativa superan la características de trabajos anteriores en términos de área y, especialmente, consumo de energía. Abstract Temperature is a first class design concern in modern integrated circuits. The important increase in power densities associated to recent technology evolutions has lead to the apparition of thermal gradients and hot spots during run time operation. Temperature impacts several circuit parameters such as speed, cooling budgets, reliability, power consumption, etc. In order to fight against these negative effects, dynamic thermal management (DTM) techniques adapt the behavior of the chip relying on the information of a monitoring system that provides run-time thermal information of the die surface. The field of on-chip temperature monitoring has drawn the attention of the scientific community in the recent years and is the object of study of this thesis. This thesis approaches the matter of on-chip temperature monitoring from different perspectives and levels, providing solutions to some of the most important issues. The physical and circuital levels are covered with the design and characterization of two novel temperature sensors specially tailored for DTM purposes. The first sensor is based upon a mechanism that obtains a pulse with a varying width based on the variations of the leakage currents on the temperature. In a nutshell, a circuit node is charged and subsequently left floating so that it discharges away through the subthreshold currents of a transistor; the time the node takes to discharge is the width of the pulse. Since the width of the pulse displays an exponential dependence on the temperature, the conversion into a digital word is realized by means of a logarithmic counter that performs both the timeto- digital conversion and the linearization of the output. The structure resulting from this combination of elements is implemented in a 0.35_m technology and is characterized by very reduced area, 10250 nm2, and power consumption, 1.05-65.5 nW at 5 samples/s, these figures outperformed all previous works by the time it was first published and still, by the time of the publication of this thesis, they outnumber all previous implementations in the same technology node. Concerning the accuracy, the sensor exhibits good linearity, even without calibration it displays a 3_ error of 1.97oC, appropriate to deal with DTM applications. As explained, the sensor is completely compatible with standard CMOS processes, this fact, along with its tiny area and power overhead, makes it specially suitable for the integration in a DTM monitoring system with a collection of on-chip monitors distributed across the chip. The exacerbated process fluctuations carried along with recent technology nodes jeop-ardize the linearity characteristics of the first sensor. In order to overcome these problems, a new temperature inferring technique is proposed. In this case, we also rely on the thermal dependencies of leakage currents that are used to discharge a floating node, but now, the result comes from the ratio of two different measures, in one of which we alter a characteristic of the discharging transistor |the gate voltage. This ratio proves to be very robust against process variations and displays a more than suficient linearity on the temperature |1.17oC 3_ error considering process variations and performing two-point calibration. The implementation of the sensing part based on this new technique implies several issues, such as the generation of process variations independent voltage reference, that are analyzed in depth in the thesis. In order to perform the time-to-digital conversion, we employ the same digitization structure the former sensor used. A completely new standard cell library targeting low area and power overhead is built from scratch to implement the digitization part. Putting all the pieces together, we achieve a complete sensor system that is characterized by ultra low energy per conversion of 48-640pJ and area of 0.0016mm2, this figure outperforms all previous works. To prove this statement, we perform a thorough comparison with over 40 works from the scientific literature. Moving up to the system level, the third contribution is centered on the modeling of a monitoring system consisting of set of thermal sensors distributed across the chip. All previous works from the literature target maximizing the accuracy of the system with the minimum number of monitors. In contrast, we introduce new metrics of quality apart form just the number of sensors; we consider the power consumption, the sampling frequency, the possibility to consider different types of monitors and the interconnection costs. The model is introduced in a simulated annealing algorithm that receives the thermal information of a system, its physical properties, area, power and interconnection constraints and a collection of monitor types; the algorithm yields the selected type of monitor, the number of monitors, their position and the optimum sampling rate. We test the algorithm with the Alpha 21364 processor under several constraint configurations to prove its validity. When compared to other previous works in the literature, the modeling presented here is the most complete. Finally, the last contribution targets the networking level, given an allocated set of temperature monitors, we focused on solving the problem of connecting them in an efficient way from the area and power perspectives. Our first proposal in this area is the introduction of a new interconnection hierarchy level, the threshing level, in between the monitors and the traditional peripheral buses that applies data selectivity to reduce the amount of information that is sent to the central controller. The idea behind this new level is that in this kind of networks most data are useless because from the controller viewpoint just a small amount of data |normally extreme values| is of interest. To cover the new interconnection level, we propose a single-wire monitoring network based on a time-domain signaling scheme that significantly reduces both the switching activity over the wire and the power consumption of the network. This scheme codes the information in the time domain and allows a straightforward obtention of an ordered list of values from the maximum to the minimum. If the scheme is applied to monitors that employ TDC, digitization resource sharing is achieved, producing an important saving in area and power consumption. Two prototypes of complete monitoring systems are presented, they significantly overcome previous works in terms of area and, specially, power consumption.

Operational Aspects of Full Reduction in Lambda Calculi

Esta tesis estudia la reducción plena (‘full reduction’ en inglés) en distintos cálculos lambda. 1 En esencia, la reducción plena consiste en evaluar los cuerpos de las funciones en los lenguajes de programación funcional con ligaduras. Se toma el cálculo lambda clásico (i.e., puro y sin tipos) como el sistema formal que modela el paradigma de programación funcional. La reducción plena es una técnica fundamental cuando se considera a los programas como datos, por ejemplo para la optimización de programas mediante evaluación parcial, o cuando algún atributo del programa se representa a su vez por un programa, como el tipo en los demostradores automáticos de teoremas actuales. Muchas semánticas operacionales que realizan reducción plena tienen naturaleza híbrida. Se introduce formalmente la noción de naturaleza híbrida, que constituye el hilo conductor de todo el trabajo. En el cálculo lambda la naturaleza híbrida se manifiesta como una ‘distinción de fase’ en el tratamiento de las abstracciones, ya sean consideradas desde fuera o desde dentro de si mismas. Esta distinción de fase conlleva una estructura en capas en la que una semántica híbrida depende de una o más semánticas subsidiarias. Desde el punto de vista de los lenguajes de programación, la tesis muestra como derivar, mediante técnicas de transformación de programas, implementaciones de semánticas operacionales que reducen plenamente a partir de sus especificaciones. Las técnicas de transformación de programas consisten en transformaciones sintácticas que preservan la equivalencia semántica de los programas. Se ajustan las técnicas de transformación de programas existentes para trabajar con implementaciones de semánticas híbridas. Además, se muestra el impacto que tiene la reducción plena en las implementaciones que utilizan entornos. Los entornos son un ingrediente fundamental en las implementaciones realistas de una máquina abstracta. Desde el punto de vista de los sistemas formales, la tesis desvela una teoría novedosa para el cálculo lambda con paso por valor (‘call-by-value lambda calculus’ en inglés) que es consistente con la reducción plena. Dicha teoría induce una noción de equivalencia observacional que distingue más puntos que las teorías existentes para dicho cálculo. Esta contribución ayuda a establecer una ‘teoría estándar’ en el cálculo lambda con paso por valor que es análoga a la ‘teoría estándar’ del cálculo lambda clásico propugnada por Barendregt. Se presentan resultados de teoría de la demostración, y se sugiere como abordar el estudio de teoría de modelos. ABSTRACT This thesis studies full reduction in lambda calculi. In a nutshell, full reduction consists in evaluating the body of the functions in a functional programming language with binders. The classical (i.e., pure untyped) lambda calculus is set as the formal system that models the functional paradigm. Full reduction is a prominent technique when programs are treated as data objects, for instance when performing optimisations by partial evaluation, or when some attribute of the program is represented by a program itself, like the type in modern proof assistants. A notable feature of many full-reducing operational semantics is its hybrid nature, which is introduced and which constitutes the guiding theme of the thesis. In the lambda calculus, the hybrid nature amounts to a ‘phase distinction’ in the treatment of abstractions when considered either from outside or from inside themselves. This distinction entails a layered structure in which a hybrid semantics depends on one or more subsidiary semantics. From a programming languages standpoint, the thesis shows how to derive implementations of full-reducing operational semantics from their specifications, by using program transformations techniques. The program transformation techniques are syntactical transformations which preserve the semantic equivalence of programs. The existing program transformation techniques are adjusted to work with implementations of hybrid semantics. The thesis also shows how full reduction impacts the implementations that use the environment technique. The environment technique is a key ingredient of real-world implementations of abstract machines which helps to circumvent the issue with binders. From a formal systems standpoint, the thesis discloses a novel consistent theory for the call-by-value variant of the lambda calculus which accounts for full reduction. This novel theory entails a notion of observational equivalence which distinguishes more points than other existing theories for the call-by-value lambda calculus. This contribution helps to establish a ‘standard theory’ in that calculus which constitutes the analogous of the ‘standard theory’ advocated by Barendregt in the classical lambda calculus. Some prooftheoretical results are presented, and insights on the model-theoretical study are given.

Mapping Dynamics into Graphs. The Visibility Algorithm

Si no tenemos en cuenta posibles procesos subyacentes con significado físico, químico, económico, etc., podemos considerar una serie temporal como un mero conjunto ordenado de valores y jugar con él algún inocente juego matemático como transformar dicho conjunto en otro objeto con la ayuda de una operación matemática para ver qué sucede: qué propiedades del conjunto original se conservan, cuáles se transforman y cómo, qué podemos decir de alguna de las dos representaciones matemáticas del objeto con sólo atender a la otra... Este ejercicio sería de cierto interés matemático por sí solo. Ocurre, además, que las series temporales son un método universal de extraer información de sistemas dinámicos en cualquier campo de la ciencia. Esto hace ganar un inesperado interés práctico al juego matemático anteriormente descrito, ya que abre la posibilidad de analizar las series temporales (vistas ahora como evolución temporal de procesos dinámicos) desde una nueva perspectiva. Hemos para esto de asumir la hipótesis de que la información codificada en la serie original se conserva de algún modo en la transformación (al menos una parte de ella). El interés resulta completo cuando la nueva representación del objeto pertencece a un campo de la matemáticas relativamente maduro, en el cual la información codificada en dicha representación puede ser descodificada y procesada de manera efectiva. ABSTRACT Disregarding any underlying process (and therefore any physical, chemical, economical or whichever meaning of its mere numeric values), we can consider a time series just as an ordered set of values and play the naive mathematical game of turning this set into a different mathematical object with the aids of an abstract mapping, and see what happens: which properties of the original set are conserved, which are transformed and how, what can we say about one of the mathematical representations just by looking at the other... This exercise is of mathematical interest by itself. In addition, it turns out that time series or signals is a universal method of extracting information from dynamical systems in any field of science. Therefore, the preceding mathematical game gains some unexpected practical interest as it opens the possibility of analyzing a time series (i.e. the outcome of a dynamical process) from an alternative angle. Of course, the information stored in the original time series should be somehow conserved in the mapping. The motivation is completed when the new representation belongs to a relatively mature mathematical field, where information encoded in such a representation can be effectively disentangled and processed. This is, in a nutshell, a first motivation to map time series into networks.

Cultura e desenvolvimento: o caso de São Tomé e Príncipe

A questão que nos propusemos analisar consiste em perceber como é que a cultura pode ser um fator de desenvolvimento e em que moldes se tem processado. Em primeiro lugar, procuraremos definir o conceito de cultura, tendo em conta as diferentes aceções que tem adquirido ao longo do tempo, para estabelecer o que é que hoje quer dizer “cultura”. No fundo, abordar de que maneira a área da cultura se interliga com outros domínios, tais como os direitos humanos, a educação, a economia, o ambiente. Também procurar debater de que modo estas áreas são fundamentais para a compreensão da noção atual de cultura e como interferem na questão do desenvolvimento. Além disso, abordaremos o papel fundamental das indústrias culturais e criativas para a compreensão do que aqui está em causa. Deste modo, daremos resposta a questões como a forma de a cultura poder ser um fator de criação de emprego, qualificação e formação e como pode ser um impulso à economia. Ao considerar que a cultura tem um caráter pragmático, lançaremos um olhar sobre a realidade de São Tomé e Príncipe, de que analisaremos os principais espaços de criatividade, as principais questões que se conjugam com o fator cultural bem como o papel que lhe é atribuído enquanto um elemento a ter em conta nas políticas públicas. Em suma, pretendemos perceber o que ainda é preciso ser feito, procurando aliar um dos pontos que constituem a chave da cultura em STP – a tradição – às exigências das novas abordagens no setor cultural.

Smart electricity grids: A very slow deployment in the EU. Egmont Paper No. 74, February 2015

Summary. The European electricity sector will have to deal with a huge challenge in the decades to come. On the one hand, electrical power is increasingly substituted for other forms of energy. It has been forecast that electricity demand will increase in the future (notably because of new needs in transport and heat sectors), although it is currently stagnant, mainly because of the economic crisis. Unless a major alternative energy source is discovered, electricity will become the central energy pillar in the long term. On the other hand, electricity production remains uncertain and will depend on numerous factors: the growth of renewable energy and decentralized energy, the renewal of old power generation capacities, increased external dependency, CO2 charges, etc. This increases the demand for electricity networks that are more reliable, more efficient, and more flexible. Europe’s current electricity networks are ageing, and, as already indicated by the International Energy Agency, many of them will need to be modernized or replaced in the decades to come. Finally, the growing impact of energy trading also needs to be taken into account. These considerations explain the need to modernize the electric grid through various ICT means. This modernization alone may allow the grid to become more flexible and interactive, to provide real time feedback, more adaptation to a fluctuating demand, and finally to reduce the global electricity costs. The paper begins with a description of the EU definition of the term ‘smart grid’ (§ 1) and of the body in charge of advising the Commission (§ 2). The EU legal framework applicable to smart grids is also detailed (§ 3). It is a rather complex domain, connected to various regulations. The paper then examines three critical factors in the development of smart grids (and smart meters as a precondition). Standardization is quite complex, but absolutely essential (§ 4). Innovation is not easily put into action (§ 5). Finally, as digital insecurity has worsened dramatically in recent years, the security of electricity networks, and especially their multiplied electronic components, will become increasingly important (§ 6). Lastly, the paper provides a concise overview of the progress of smart grids in the EU in recent years (§ 7). In a nutshell, the conclusion is that progress is quite slow, many obstacles remain, and, given the appearance of many new regulatory problems, it would be useful to organize a review of the present EU strategy.

Light and shadows in Europe’s new Action Plan for Capital Markets Union. ECMI Commentary No. 40/5 October 2015

The European Commission’s Action Plan consists, in a nutshell, of a short list of technical proposals and a longer one of (rather general) potential actions. Overall, the plan indeed proposes to achieve some short-term objectives, such as a reduction of listing costs for SMEs, but it lacks long-term vision. The plan bundles actions under rather generic objectives of long-term finance or cross-border investing. Improving the informational infrastructure (e.g. accounting standards, company data) and cross-border enforcement of rules is left to vaguely defined future actions, but these constitute the core of the capital markets infrastructure. Without a well-defined set of measurable objectives, the whole plan may lose political momentum and become an opportunity for interested parties to cherry pick their pet provisions. Building a single market, i.e. removing cross-border obstacles to capital circulation, is too challenging a task to simply appear as one of many items on a long list of general objectives, which incidentally do not include institutional reform. The ultimate risk is that the Commission may just miss a unique opportunity to revamp and improve the financial integration process in Europe after almost a decade of harmful financial retrenchment.

Regulation on ‘cross-border portability’ of online content services: Roaming for Netflix or the end of copyright territoriality? CEPS Commentary, 15 February 2016

In a communication to the Parliament and the Council entitled “Towards a modern, more European copyright framework” and dated 9 December 2015,1 the European Commission confirmed its intention to progressively remove the main obstacles to the functioning of the Digital Single Market for copyrighted works. The first step of this long-term plan, which was first announced in Juncker’s Political Guidelines2 and the Communication on “A Digital Single Market strategy for Europe”,3 is a proposal for a regulation aimed at ensuring the so-called ‘cross-border portability’ of online services giving access to content such as music, games, films and sporting events.4 In a nutshell, the proposed regulation seeks to enable consumers with legal access to such online content services in their country of residence to use the same services also when they are in another member state for a limited period of time. On the one hand, this legislative proposal has the full potential to resolve the (limited) issue of portability, which stems from the national dimension of copyright and the persisting territorial licensing and distribution of copyright content.5 On the other hand, as this commentary shows, the ambiguity of certain important provisions in the proposed regulation might affect its scope and effectiveness and contribute to the erosion of the principle of copyright territoriality.

The farmer's encyclopedia and business guide : a repository of practical knowledge /

Issued in 1889 under title "The little giant cyclopedia", and in 1893 under title "The marvel cyclopedia". Also issued under titles "The nutshell cyclopedia" and "Armstrong's treasury of ready reference.

Proceedings ... annual convention.

Mode of access: Internet.

Around the Capital with Uncle Hank, recorded together with many pictures,

Mode of access: Internet.

Report of proceedings of the annual convention.

Mode of access: Internet.

Farmers’ Market Nutrition Program Recipe Cards

These are cards giving recipes for fruit and vegetable dishes. Recipes include: confetti bean salsa, Mediterranean quinoa salad, minty watermelon cucumber salad, quick refrigerator pickles, broccoli salad, apple, cranberry and almond coleslaw, farmers’ market pasta salad, roasted beet and butter bean hummus, spinach and strawberry pecan salad, okra, avocado and tomato salad, plum-berry mint smoothie and crispy baked vegetables.

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.