Sokolsky, Oleg

Profile Picture
Email Address
ORCID
Disciplines
Computer Sciences
Software Engineering
Research Projects
Organizational Units
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

Filters

171
124232031
Reset filters

Settings

Search Results

Now showing 1 - 10 of 171
  • Publication
    Extensible Energy Planning Framework for Preemptive Tasks
    (2017-05-01) Kim, Jin Hyun; Gangadharan, Deepak; Sokolsky, Oleg; Lee, Insup; Legay, Axel
    Cyber-physical systems (CSPs) are demanding energy-efficient design not only of hardware (HW), but also of software (SW). Dynamic Voltage and and Frequency Scaling (DVFS) and Dynamic Power Manage (DPM) are most popular techniques to improve the energy efficiency. However, contemporary complicated HW and SW designs requires more elaborate and sophisticated energy management and efficiency evaluation techniques. This paper is concerned about energy supply planning for real-time scheduling systems (units) of which tasks need to meet deadlines. This paper presents a modelbased compositional energy planning technique that computes a minimal ratio of processor frequency that preserves schedulability of independent and preemptive tasks. The minimal ratio of processor frequency can be used to plan the energy supply of real-time components. Our model-based technique is extensible by refining our model with additional features so that energy management techniques and their energy efficiency can be evaluated by model checking techniques. We exploit the compositional framework for hierarchical scheduling systems and provide a new resource model for the frequency computation. As results, our use-case for avionics software components shows that our new method outperforms the classical real-time calculus (RTC) method, requiring 36.21% less frequency ratio on average for scheduling units under RM than the RTC method.
  • Publication
    A Safety-Assured Development Approach for Real-Time Software
    (2010-08-23) Jee, Eunkyoung; Wang, Shaohui; Kim, Jeong Ki; Lee, Jaewoo; Sokolsky, Oleg; Lee, Insup
    Guaranteeing timing properties is an important issue as we develop safety-critical real-time systems such as cardiac pacemakers. We present a safety assured development approach of real-time software using a pacemaker as our case study. Following the model-driven development techniques, measurement-based timing analysis is used to guarantee timing properties in implementation as well as in the formal model. Formal specification with timed automata is checked with respect to timing properties by model checking technique and is transformed into implementation systematically. When timing properties may be violated in the implementation due to timing delay, it is suggested to measure the time deviation and reflect it to the code explicitly by modifying guards. The model is altered according to the modifications in the code. These changes of the code and the model are considered safe if all the properties are still satisfied by the modified model in re-performed model hecking. We demonstrate how the suggested approach can be applied to single-threaded and multi-threaded versions of implementation. This approach can provide developers with a useful time-guaranteeing technique applicable to several code generation schemes without imposing many restrictions.
  • Publication
    A Framework for Reasoning About Animation Systems
    (2001-01-01) Aaron, Eric; Metaxas, Dimitris; Ivancic, Franjo; Sokolsky, Oleg
    In this paper, we consider the potential for reasoning about animations in the language of hybrid dynamical systems (i.e., systems with both continuous and discrete dynamics). We begin by directly applying hybrid systems theory to animation, using a general-purpose hybrid system specification tool to generate multi-agent animations; this application also illustrates that hybrid system models can provide systematic modular ways to incorporate low-level behavior into a design for higher-level behavioral modeling. We then apply the logical framework of hybrid systems to animation: we formally state properties of animation systems that may not be readily expressed in other frameworks; and we mechanically check a collision-avoidance property for a simple race-like game. This hybrid systems-oriented approach could improve our ability to reason about virtual worlds, thus improving our ability to create intelligent virtual agents.
  • Publication
    Analysis of AADL Models Using Real-Time Calculus With Applications to Wireless Architectures
    (2008-07-23) Sokolsky, Oleg; Chernoguzov, Alexander
    Architecture Analysis and Design Language (AADL) captures both platform and software architectures of embedded systems in a component oriented fashion. Properties embedded in an AADL model enable several high-level analysis techniques. In this work, we explore how to perform analysis of end-to-end timing characteristics of an AADL model using Real-Time Calculus (RTC). We identify properties of AADL models that are necessary to enable such analysis and develop an algorithm to transform an AADL model into an RTC model.
  • Publication
    Scalable Verification of Linear Controller Software
    (2016-04-01) Park, Junkil; Lee, Insup; Sokolsky, Oleg; Pajic, Miroslav
    We consider the problem of verifying software implementations of linear time-invariant controllers against mathematical specifications. Given a controller specification, multiple correct implementations may exist, each of which uses a different representation of controller state (e.g., due to optimizations in a third-party code generator). To accommodate this variation, we first extract a controller's mathematical model from the implementation via symbolic execution, and then check input-output equivalence between the extracted model and the specification by similarity checking. We show how to automatically verify the correctness of C code controller implementation using the combination of techniques such as symbolic execution, satisfiability solving and convex optimization. Through evaluation using randomly generated controller specifications of realistic size, we demonstrate that the scalability of this approach has significantly improved compared to our own earlier work based on the invariant checking method.
  • Publication
    Bandwidth Optimal Data/Service Delivery for Connected Vehicles via Edges
    (2018-07-01) Gangadharan, Deepak; Sokolsky, Oleg; Lee, Insup; Kim, BaekGyu; Lin, Chung-Wei; Shiraishi, Shinichi
    The paradigm of connected vehicles is fast gaining lot of attraction in the automotive industry. Recently, a lot of technological innovation has been pushed through to realize this paradigm using vehicle to cloud (V2C), infrastructure (V2I) and vehicle (V2V) communications. This has also opened the doors for efficient delivery of data/service to the vehicles via edge devices that are closer to the vehicles. In this work, we propose an optimization framework that can be used to deliver data/service to the connected vehicles such that a bandwidth cost objective is optimized. For the first time, we also integrate a vehicle flow model in the optimization framework to model the traffic flow in the coverage area of the edges. Using the optimization framework, we study the variation of the optimal bandwidth cost for varying problem sizes and vehicle flow model parameter values for both data and service delivery.
  • Publication
    Functional Alarms for Systems of Interoperable Medical Devices
    (2014-01-09) Venkatasubramanian, Krishna; Vasserman, Eugene; Sokolsky, Oleg; Lee, Insup
    Alarms are essential for medical systems in order to ensure patient safety during deteriorating clinical situations and inevitable device malfunction. As medical devices are connected together to become interoperable, alarms become crucial part in making them high-assurance, in nature. Traditional alarm systems for interoperable medical devices have been patient-centric. In this paper, we introduce the need for an alarm system that focuses on the correct functionality of the interoperability architecture itself, along with several considerations and design challenges in enabling them.
  • Publication
    Declarative Network Verification
    (2008-12-23) Wang, Anduo; Basu, Prithwish; Loo, Boon Thau; Sokolsky, Oleg
    In this paper, we present our initial design and implementation of a declarative network verifier (DNV). DNV utilizes theorem proving, a well established verification technique where logic-based axioms that automatically capture network semantics are generated, and a user-driven proof process is used to establish network correctness properties. DNV takes as input declarative networking specifications written in the Network Datalog (NDlog) query language, and maps that automatically into logical axioms that can be directly used in existing theorem provers to validate protocol correctness. DNV is a significant improvement compared to existing use case of theorem proving which typically require several man-months to construct the system specifications. Moreover, NDlog, a high-level specification, whose semantics are precisely compiled into DNV without loss, can be directly executed as implementations, hence bridging specifications, verification, and implementation. To validate the use of DNV, we present case studies using DNV in conjunction with the PVS theorem prover to verify routing protocols, including eventual properties of protocols in dynamic settings.
  • Publication
    AS-TRUST: A Trust Characterization Scheme for Autonomous Systems in BGP
    (2010-01-01) Kannan, Sampath; Chang, Jian; Loo, Boon Thau; Venkatasubramanian, Krishna K.; Sokolsky, Oleg; West, Andrew G.; Lee, Insup
    Border Gateway Protocol (BGP) works by frequently exchanging updates which, disseminate reachability information (RI) about IP prefixes (i.e., address blocks) between Autonomous Systems (ASes) on the Internet. The current operation of BGP implicitly trusts the ASes to disseminate valid—accurate, stable and routing policy compliant — RI. This assumption is problematic as demonstrated by the recent documented instances of invalid RI dissemination. This paper presents AS-TRUST, a scheme which comprehensively characterizes the trustworthiness of ASes, with respect to disseminating valid RI. AS-TRUST quantifies trust using the notion of reputation. To compute reputation, AS-TRUST evaluates the past RI received for validity, based on a set of well-defined properties. It then classifies the resulting observations into multiple types of feedback. The feedback is used by a reputation function to compute a probabilistic view of AS trustworthiness. The contributions of the paper are: (1) a comprehensive trust characterization of ASes; (2) a set of well-defined properties for evaluating the validity of RI provided by ASes; and (3) a novel and theoretically sound reputation computation mechanism. Our implementation of AS-TRUST scheme using publicly available BGP traces demonstrates: the number of ASes involved in violating the BGP operational trust assumption is significant, dissemination of invalid RI is consistently present, and the proposed reputation mechanism is sensitive enough to capture even rare instances of an AS’ deviation from trustworthy behavior.
  • Publication
    Multi-Mode Virtualization for Soft Real-Time Systems
    (2018-04-01) Xu, Meng; Li, Haoran; Phan, Linh T.X.; Li, Chong; Lee, Insup; Lu, Chenyang; Sokolsky, Oleg; Gill, Christopher
    Real-time virtualization is an emerging technology for embedded systems integration and latency-sensitive cloud applications. Earlier real-time virtualization platforms require offline configuration of the scheduling parameters of virtual machines (VMs) based on their worst-case workloads, but this static approach results in pessimistic resource allocation when the workloads in the VMs change dynamically. Here, we present Multi-Mode-Xen (M2-Xen), a real-time virtualization platform for dynamic real-time systems where VMs can operate in modes with different CPU resource requirements at run-time. M2-Xen has three salient capabilities: (1) dynamic allocation of CPU resources among VMs in response to their mode changes, (2) overload avoidance at both the VM and host levels during mode transitions, and (3) fast mode transitions between different modes. M2-Xen has been implemented within Xen 4.8 using the real-time deferrable server (RTDS) scheduler. Experimental results show that M2-Xen maintains real-time performance in different modes, avoids overload during mode changes, and performs fast mode transitions.