 |
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. | |
| 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. | |
| Modeling and analysis of medical devices and systems | |
| |
| 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.
| |
| 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: | |
| 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 | |
| |