Seminars

Type 1 diabetes (T1D) is an autoimmune disease that causes the destruction of the pancreatic beta cells, permanently suppressing insulin secretion and requiring patients to manually inject or infuse insulin to keep blood sugar levels close to normal.  Self-treatment of T1D can be regarded as a closed-loop control system with a significant “human-in-the-loop” aspect.  Artificial pancreas (AP) systems seek to both improve glycemic outcomes and reduce cognitive burden associated with self-treatment by taking advantage of modern glucose monitoring and insulin pump technology.  While the…

We begin by presenting a very short overview of past and current research carried out by the Safety Critical Avionics Brach (SCAB) at NASA's Langley Research Center (LaRC). We will then discuss several ongoing and new research projects being conducted in the SCAB. In particular, we will survey new research efforts in safety-critical fault-tolerant distributed avionics, verification of numerical software, and run-time verification as well as experiments involving unmanned aerial systems (UAS). We will discuss opportunities for internships in each of these projects as well as areas such as…

In this talk, I will try to make a case for the use of data flow graphs as a suitable notion for abstractions of concurrent programs for the purpose of verification. I will talk about two successful experiences that we have had with these graphs. One is the development of an abstract interpretation framework that constructs annotated data flow graph where the annotations can come from any abstract domain such as intervals or octagons. We demonstrate how by separating the concerns of reasoning about data (computing the data invariants) and control (computing a precise enough pattern of…

There is a growing demand for systems that can detect complex patterns in high-speed streams of events or in large volumes of stored sequences. This demand is driven by so-called complex event processing (CEP) applications whose success depends on their ability to make real-time decisions, such as high-frequency trading, fraud detection, and online advertisement. As a result, several database vendors are providing new SQL extensions to support such applications.

In this talk, we show that these extensions suffer from expressivity limitations that severely impair their generality…

(Joint work with Gethin Norman and David Parker) 

Quantitative verification techniques are able to establish system properties such as "the probability of an airbag failing to deploy on demand'' or "the expected time for a network protocol to successfully send a message packet''. In this paper, we describe a framework for quantitative verification of software that exhibits both real-time and probabilistic behaviour. The complexity of real software, combined with the need to capture precise timing information, necessitates the use of abstraction techniques. We outline a…