Oleg Sokolsky

Research Associate Professor


 Address:
Department of Computer and Information Science
University of Pennsylvania
3330 Walnut Street
Philadelphia, PA 19104-6389
Phone: (215) 898-4448
Fax: (215) 898-0587
Office: 608 Levine
E-mail:
sokolsky@cis.upenn.edu
I am a Research Associate Professor with the Department of Computer and Information Science of University of Pennsylvania. I am a member of the PRECISE Center (Penn Research in Embedded Computing and Integrated Systems), and Real-Time Systems group. See my Curriculum Vita for full detail.

Research Interests
My main research interest is the application of formal methods to design and verification of distributed real-time systems. Other interests, all related to the main one, include on-line monitoring of distributed systems and formal foundations for it, hybrid systems, automated extraction of specifications from source code, and formal methods in software engineering in general and in embedded software in particular.

Please see my publications on these topics.

Upcoming talks:
Conferences I am involved in (or was involved in recently)
Current Projects
Besides several small things, I am currently involved in the following big projects.
Attack-resilient control systems
  • The SPARCS project, part of the DARPA HACMS program, is exploring techniques to make control systems resilient to a variety of external attacks, including attacks on sensors that affect fidelity of sensor readings. We are also studying means of high-assurance implementation of resilient control designs.
Modeling and analysis of medical devices and systems
  • Generic Infusion Pump (GIP) is a project to develop requirements for infusion pumps and a reference implementation for such a pump. The intent of the effort is to provide a platform for experimentation for the academic embedded systems community.
  • Medical device interoperability requires new approaches to safety analysis and regulatory approval. To support dynamically deployed multi-device clinical applications, we are developing an interoperability platform to provide isolation of different applications in terms of timing and quality of service. We are also exploring clinical applications that are enabled by medical device interoperability, including physiological closed-loop control.
  • We are paticipating in the pacemaker challenge
Resource interfaces for real-time systems
We are developing the notion of a component for the construction and compositional analysis of real-time systems. Components export their resource requirements in order to allow modular composition that preserves timing properties of the system.
Quantitative trust management (QTM)
QTM is a novel approach to access control under uncertainty combines credential-based trust with reputation from past interactions. The project also explores applications of reputation-based techniques to autonomous system credibility and vandalism detection. Funded by an ONR MURI.

A follow-up project applies QTM ideas to the area of crowd-sourced, model-based manufacturing. We are building a flexible access control system from such an environment. Funded by the DARPA AVM program.

Architectural modeling of embedded systems.
We are developing tool support for the analysis of embedded systems architectures expressed in the AADL modeling language. I am a member of the AADL standardization committee.
  • We developed the Furness toolset in collaboration with Fremont Associates, which includes an AADL simulator and algorithms for formal schedulability analysis of AADL models;
  • We studied performance analysis of wireless architectures in a case study performed in collaboration with Honeywell.
Run-time Monitoring and Checking
The Monitoring and Checking project concentrates on run-time verification of software systems. The MaC tool checks formally specified properties of executions of Java applications.

A recently completed related ONR MURI project explores the application of monitoring and checking to computer security.

Past Projects
Modeling with hierarchical hybrid systems.
The modeling environment is provided by the modeling language CHARON and its toolset. CHARON modeling approach has been extensively used in two domains:
  • Modeling of embedded software, especially automotive controllers, has been performed in the MoBIES (Model-Based Integration of Embedded Software) program (over as of 1/04).
  • Modeling of biological systems in the BioComp program (over as of 1/06).
HASTEN (High Assurance Systems Tools and Environments) was devoted to practical integration of different formal methods and domain-specific specialization of formalisms.
MoBIES (Model Based Integration of Embedded Systems) was a great DARPA project, which all participants fondly remember.
My previous work in formal methods concentrated on the tools for formal specification and verification, including Concurrency Factory and PARAGON. I was also designing algorithms for different flavours of model checking.

You may want to see my list of publications. Some of the work presented there has been accomplished during my Ph.D. studies at the State University of New York at Stony Brook. Professor Scott A. Smolka was my advisor. My thesis is available in the PostScript format.

Education

Personal Information

Last updated November 14, 2011.