|
|
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 Real-Time Systems
group and the
Hybrid 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 components for the construciton of real-time systems. Component export their resource requirements in order to allow modular composition of real-time systems. | |
| Architectural modeling of embedded systems. | |
We partner with Fremont Associates to
provide tool support for analysis of embedded systems architectures expressed
in the AADL modeling language. Formal
schedulability analysis algorithms are implemented in the Furness toolset.
| |
| 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. | |
| 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: | |
| Past Projects | |
| HASTEN (High Assurance Systems Tools and Environments) is a recently completed project devoted to practical integration of different formal methods and domain-specific specialization of formalisms. | |
|
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 | |
| |