Event

MBSE Colloquium: Sandeep Shukla, "Models of Time for Safety Critical Systems"

Monday, October 7, 2013
11:00 a.m.
1146 A.V. Williams Building
Kimberly Edwards
kedwards@umd.edu

Model-Based Systems Engineering Colloquium
Models of Time for Safety Critical Systems
Partial vs. Total Order--Polychronous vs. Synchronous

Sandeep Shukla
Professor of Electrical and Computer Engineering
Hume Center for National Security and Technology
Virginia Tech Arlington Research Center

| video | slides |

Host
John Baras

Abstract
In safety critical systems, accuracy of time is important if the activities of the system are time driven, and the notion of synchrony is based on the accuracy of time. The synchronization of clocks for such systems and protocols come at the cost of an overhead of running expensive synchronization algorithms. Moreover, in recent times, systems dependent on precise clock synchronization are vulnerable to cyber-attacks. In the context of embedded real-time systems models of time have been a subject of intense research in the past two decades. Today’s systems with multi-tasking, multi-threading, and multi-core precepts have naturally multiple notions of time. This gives us the notion of polychronous time. Thus time is no longer unique or the same at all concurrently running entities, but they have their own totally ordered instants as their local times, and the instants in these local time sets are partially ordered with respect the instants in another thread’s local time. Thus polychronous notion of time frees us from the requirements of strong clock synchronization, and work at maximal performance in between synchronization points. In order to free the programming model from synchronous timing model, and making systems robust to clock synchronization failure based attacks; we have been advocating polychronous model of computation for concurrent systems. However, we do not advocate that programmers design programs against this model manually, or prove correctness themselves. We propose a dataflow model of computation which describes only the intended computation as a set of concurrent dataflows, and a program synthesis technique synthesizes multi-threaded code from such specifications. The generated code does not depend on clock synchronization, and each thread has local notion of time which are totally ordered themselves, and partially ordered globally. The correctness proof obligation is no longer with the implementer but with the modeler who would prove the properties on the concurrent dataflow model. The program synthesis engine of course has to be proven correct in order to claim correctness of the generated code from the model.

Biography
Sandeep K. Shukla is a professor of Electrical and Computer Engineering at Virginia Tech. He has published more than 200 conference papers, book chapters, and journal articles. He also co-edited or co-authored nine books. He is a recipient of the PECASE award, NSF CAREER award, Humboldt foundation’s Bessel award, a best paper award etc. He is an IEEE computer society distinguished visitor and an ACM visiting speaker. He is an ACM Distinguished Scientist. He is currently working with the US Air Force to develop techniques and tools for multi-threaded code synthesis from polychronous specifications. Model of time in computational model is one of his major topics of interest. His other research areas are in formal methods applications to cyber security, safety-critical embedded system modeling and synthesis, formal verification, smart-grid and SCADA security models.

Audience: Graduate  Undergraduate  Faculty  Post-Docs  Alumni  Corporate