Oleg Sokolsky

Research 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: Levine 608 E-mail: sokolsky@cis.upenn.edu
I am a Research 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 ensuring safety of real-time and cyber-physical systems (CPS). Other interests, all related to the main one, include the application of formal methods in design and verification of CPS, on-line monitoring of embedded and cyber-physical 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. Although the word formal is repeated often in the previous sentence, I am more interested in exploring the boundary between formal and informal, and in carrying safety guarantees across the boundary, then in developing new formal techniques. Please see my publications on these topics.
Current Projects
Besides several small things, I am currently involved in the following big projects.
Dynamic assurance for autonomous systems with learning-based components
As part of the DARPA Assured Autonomy program, we are exploring techniques for verification of cyber-physical systems that contain learning-based components, and generation of monitors that alert us when these components appear to be misbehaving. We are also studying construction of assurance cases for systems that rely on this monitoring.
Attack-resilient control systems
The SPARCS project, part of the DARPA HACMS program, was exploring techniques to make control systems resilient to a variety of external attacks, including attacks on sensors that affect fidelity of sensor readings. We have also studied means of high-assurance implementation of resilient control designs. The HACMS program is over as of 2017. A follow-up project explores the concept of checkpointing and recovery for the control systems.
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
Run-time Monitoring and Checking
The Monitoring and Checking project concentrates on run-time verification of software systems. The MaC tool, which checks formally specified properties of executions of Java applications, is one of the first runtime verification tools. An on-going follow-up project, pursued jointly with BAE and funded by the DARPA BRASS program, aims to apply runtime verification in the context of intent monitoring. The goal is to trigger and guide dynamic adaptation of long-living software when intent deviations are detected. As part of this project, we are developing a successor tool to MaC, which would fully support parametric monitoring and combination of synchronous and asynchronous monitors.
Past Projects
Resource interfaces for real-time systems
We have developed 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. Component-based hierarchical schedulability analysis is supported by the tool CARTS.
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.
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.
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.
Community Service
Conferences I am involved in (or was involved in recently)
Cyber-Physical Systems Week, April 21-24, 2020 virtually in Sydney, Australia 20th International Conference on Runtime Verification, October 6-9, 2020, in Los Angeles, USA 18th International Symposium on Automated Technology for Verification and Analysis (ATVA), October 19-23, 2020, in Hanoi, Vietnam
Editorial duties
I am a member of the editorial board of IEEE Embedded Systems Letters, ACM Transactions on Embedded Computing Systems, and Smart Health journals and IEEE Computer. I have been the editor of the ACM SIGBED Review newsletter through July 2019.
Education
Ph.D. (Computer Science), SUNY Stony Brook, 1996. B.Sc./M.Sc. (Computer Science), St. Petersburg State Technical University, 1988. Some of the work presented in my list of publications 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.

Last updated July 22, 2020.