Sokolsky, Oleg
Loading...
Email Address
ORCID
Disciplines
Computer Sciences
Software Engineering
Software Engineering
relationships.isProjectOf
relationships.isOrgUnitOf
Position
Research Professor
Introduction
My main research interest is the application of formal methods to design and verification of cyber-physical systems. Other interests, all related to the main one, include on-line monitoring of embedded 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.
Research Interests
Collection
171 results
Search Results
Now showing 1 - 10 of 171
Publication A Retrospective Look at the Monitoring and Checking (MaC) Framework(2019-10-01) Kannan, Sampath; Lee, Insup; Sokolsky, Oleg; Kim, Moonzoo; Viswanathan, MaheshThe Monitoring and Checking (MaC) project gave rise to a framework for runtime monitoring with respect to formally specified properties, which later came to be known as runtime verification. The project also built a pioneering runtime verification tool, Java-MaC, that was an instantiation of the approach to check properties of Java programs. In this retrospective, we discuss decisions made in the design of the framework and summarize lessons learned in the course of the project.Publication RT-MaC: Runtime Monitoring and Checking of Quantitative and Probabilistic Properties(2005-08-17) Sammapun, Usa; Lee, Insup; Sokolsky, OlegCorrectness of a real-time system depends on its computation as well as its timeliness and its reliability. In recent years, researches have focused on verifying correctness of a real-time system during runtime by monitoring its execution and checking it against its formal specifications. Such verification method is called Runtime Verification. Most existing runtime verification tools verify computation correctness using qualitative property specifications but do not verify timeliness nor reliability correctness. In this paper, we investigate the verification on timeliness and reliability correctness by offering quantitative and probabilistic property specifications and implementing efficient verifiers.Publication Towards Assurance for Plug & Play Medical Systems(2015-09-01) King, Andrew L.; Feng, Lu; Chen, Sanjian; Sokolsky, Oleg; Lee, Insup; Procter, Sam; Hatcliff, JohnTraditional safety-critical systems are designed and integrated by a systems integrator. The system integrator can asses the safety of the completed system before it is deployed. In medicine, there is a desire to transition from the traditional approach to a new model wherein a user can combine various devices post-hoc to create a new composite system that addresses a specific clinical scenario. Ensuring the safety of these systems is challenging: Safety is a property of systems that arises from the interaction of system components and it’s not possible to asses overall system safety by assessing a single component in isolation. It is unlikely that end-users will have the engineering expertise or resources to perform safety assessments each time they create a new composite system. In this paper we describe a platform-oriented approach to providing assurance for plug & play medical systems as well as an associated assurance argument pattern.Publication Towards Synthesis of Platform-Aware Attack-Resilient Control Systems: Extended Abstract(2013-04-09) Pajic, Miroslav; Bezzo, Nicola; Weimer, James; Alur, Rajeev; Mangharam, Rahul; Michael, Nathan; Pappas, George J; Sokolsky, Oleg; Tabuada, Paulo; Weirich, Stephanie; Lee, InsupPublication Data-driven Adaptive Safety Monitoring using Virtual Subjects in Medical Cyber-Physical Systems: A Glucose Control Case Study(2016-09-01) Chen, Sanjian; Sokolsky, Oleg; Weimer, James; Lee, InsupMedical cyber-physical systems (MCPS) integrate sensors, actuators, and software to improve patient safety and quality of healthcare. These systems introduce major challenges to safety analysis because the patient’s physiology is complex, nonlinear, unobservable, and uncertain. To cope with the challenge that unidentified physiological parameters may exhibit short-term variances in certain clinical scenarios, we propose a novel run-time predictive safety monitoring technique that leverages a maximal model coupled with online training of a computational virtual subject (CVS) set. The proposed monitor predicts safety-critical events at run-time using only clinically available measurements. We apply the technique to a surgical glucose control case study. Evaluation on retrospective real clinical data shows that the algorithm achieves 96% sensitivity with a low average false alarm rate of 0.5 false alarm per surgery.Publication DMaC: Distributed Monitoring and Checking(2009-06-01) Zhou, Wenchao; Sokolsky, Oleg; Loo, Boon Thau; Lee, InsupWe consider monitoring and checking formally specified properties in a network. We are addressing the problem of deploying the checkers on different network nodes that provide correct and efficient checking. We present the DMaC system that builds upon two bodies of work: the Monitoring and Checking (MaC) framework, which provides means to monitor and check running systems against formally specified requirements, and declarative networking, a declarative domain-specific approach for specifying and implementing distributed network protocols. DMaC uses a declarative networking system for both specifying network protocols and performing checker execution. High-level properties are automatically translated from safety property specifications in the MaC framework into declarative networking queries and integrated into the rest of the network for monitoring the safety properties. We evaluate the flexibility and efficiency of DMaC using simple but realistic network protocols and their propertiesPublication Overhead-Aware Deployment of Runtime Monitors(2019-10-01) Zhang, Teng; Lee, Insup; Sokolsky, Oleg; Eakman, GregOne important issue needed to be handled when applying runtime verification is the time overhead introduced by online monitors. According to how monitors are deployed with the system to be monitored, the overhead may come from the execution of monitoring logic or asynchronous communication. In this paper, we present a method for deciding how to deploy runtime monitors with awareness of minimizing the overhead. We first propose a parametric model to estimate the overhead given the prior knowledge on the distribution of incoming events and the time cost of sending a message and executing monitoring logic. Then, we will discuss how to statically decide the boundary of synchronous and asynchronous monitors such that the lowest overhead can be obtained.Publication High-Level Model Extraction via Symbolic Execution(2012-01-01) Wang, Shaohui; Dwarakanathan, Srinivasan; Sokolsky, Oleg; Lee, InsupWe study the problem of extracting high-level state machine models from software source code. Our target domain is GUI-driven applications for small hand-held devices such as cell phones and PDAs. In such systems, a natural high-level model is captured by a state machine, where states are GUI screens and button/menu item tappings are actions that trigger transitions between states. The paper presents a symbolic execution technique that allows us to identify states and transitions from the application source code. We discuss an implementation of this technique that operates on a large subset of the C# language and apply as a case study to the subsystem of a decision support tool for medical diagnosis.Publication Schedulability Analysis of AADL models(2006-04-29) Sokolsky, Oleg; Lee, Insup; Clark, DuncanThe paper discusses the use of formal methods for the analysis of architectural models expressed in the modeling language AADL. AADL describes the system as a collection of interacting components. The AADL standard prescribes semantics for the thread components and rules of interaction between threads and other components in the system. We present a semantics-preserving translation of AADL models into the real-time process algebra ACSR, allowing us to perform schedulability analysis of AADL models.Publication Process Algebraic Modeling and Analysis of Power-Aware Real-Time Systems(2002-08-01) Lee, Insup; Sokolsky, Oleg; Philippou, AnnaThe paper describes a unified formal framework for designing and reasoning about power-constrained, real-time systems. The framework is based on process algebra, a formalism which has been developed to describe and analyze communicating, concurrent systems. The proposed extension allows the modeling of probabilistic resource failures, priorities of resource usages, and power consumption by resources within the same formalism. Thus, it is possible to evaluate alternative power-consumption behaviors and tradeoffs under different real-time schedulers, resource limitations, resource failure probabilities, etc. This paper describes the modeling and analysis techniques, and illustrates them with examples, including a dynamic voltage-scaling algorithm.