Carnegie Mellon University
Software and Societal Systems Department  ›  Software Engineering Ph.D. Program  ›  People  ›  Alumni  ›  alumni-bios  ›  Ivan Ruchkin

Ivan Ruchkin

Dr. Ivan Ruchkin

Address
5000 Forbes Avenue
Pittsburgh, PA 15213

Bio

What I do 

My current research area is formal modeling, analysis, and verification for cyber-physical systems (CPS). I am particularly interested in creating methodologies and modeling tools to enable correct and effective integration of diverse modeling methods for CPS. To this end, my research employs a variety of formal approaches and algorithmic techniques.

Want to learn more? For a popular summary of my research, see "Modeling from the Ground Up" (pages 20-22). For more details, go to my research page or check out my slides.

What I did before

I grew up in Moscow, Russia and received a degree in Applied Math & Computer Science from Lomonosov Moscow State University. Prior to joining CMU, I worked as a part-time software engineer and a UI designer for several years, and did research on the intersection of Human-Computer Interaction and Software Engineering. In that work, I reduced the proliferation of tool windows in integrated development environments.

Research

Integration of Modeling Methods for Cyber-Physical Systems

Modern cyber-physical systems (CPS), like autonomous drones and self-driving cars, are particularly demanding of rigorous quality assurance because of their impact on our lives. This assurance often relies on diverse modeling methods from a broad range of scientific and engineering fields, from optimization algorithms to mechanical engineering.

Diverse models and analyses are difficult integrate (i.e., use in combination towards a shared goal) due to their complexity and heterogeneity. When they are combined in an ad hoc way, inconsistencies may emerge between models, potentially leading to critical failures in CPS. Even if models are made consistent at some point, uncontrolled changes (both manual and automated) to models may violate that consistency.

My dissertation develops an augmented architectural approach (see the image) to integration of CPS modeling methods. This approach relies on architectural views (i.e., component-and-connector models annotated with types and properties) to represent and check integration-relevant information from detailed CPS models (e.g., hybrid programs).

The augmented architectural approach relies on three novel integration techniques. First, automated model-view relations preserve the correspondence between models and their respective views using domain-specific model transformations. To prevent inconsistencies caused by automated analyses, I use the second technique – formal specification of analysis contracts (see below). Finally, to detect complex inconsistencies that span several models, I develop the third technique – an integration property language, which engineers can use to specify assumptions, guarantees, and consistency statements over heterogeneous models and views.

Learn more:

  • Details on modeling method integration are in this paper.
  • Future ideas about integration are in this paper.

Model-Based Adaptation for Robotic Systems (MARS)

Mobile robots can accomplish increasingly impressive feats, but don't stay deployed for long periods of time. As years pass, the technology becomes too complex and expensive to maintain and evolve, and is declared obsolete. The underlying problem is the low level of abstraction at which robotics code is written, making code difficult to evolve. Local fixes in the code enable low-level adaptation, they but make the code even more brittle to larger-scale changes.

This Model-Based Adaptation for Robotic Systems (MARS) project aims to raise the level of abstraction at which we adapt robotic systems. To this end, we apply a coordinated set of models to automate adaptation, which includes changing sensors, actuators, and software components. As the image above suggests, this model-based adaptation is more manageable, automated, and efficient than manual adaptation of code. The project is carried out based on the TurtleBot open-source robotic platform.

My role in this project is to build physical models (such as ones for power and motion) for Turtlebot and envision adaptation based on them. Since we use multiple models to power adaptation, MARS is also a fitting context to apply my model integration techniques.

Learn more:

  • We reflected on challenges in physical modeling in this paper.
  • A couple of TurtleBot power data collection videos are available here and here.

Analysis Contracts for Cyber-Physical Systems

Designing a high-quality cyber-physical system, like an autonomous car, requires combined engineering for its cyber and physical aspects: control stability, planning, schedulability, protocol correctness, thermal safety, and energy efficiency -- to name a few. Development of these aspects relies upon various domains of engineering expertise for appropriate system models and analytic operations on these models. For example, signal-flow graphs and simulation (e.g., in Simulink) are appropriate to analyze a controller's stability, while state machines and reachability analysis can be used to ensure protocol correctness.

Analyses from different domains may deliver unsound results if their often-implicit assumptions are compromised. Such assumptions may concern complicated behaviors: for instance, the bin packing algorithm for thread-to-processor allocation is only applicable if the scheduling policy is equivalent to deadline-monotonic. So a major research question of multi-model CPS design is, how can we specify and verify correctness of co-operative multi-domain analyses in practice?

I developed a methodology to combine analyses based on analysis contracts. These contracts describe data inputs and outputs of each analysis, as well as its assumptions and guarantees. Using this specification, we can algorithmically verify correctness of analysis application using domain-specific models and verification techniques. The image above shows an example set of analyses for two domains: thread scheduling and design battery. The analysis contracts methodology is embodied in a tool called ACTIVE(Analysis Contract Integration Verifier) that builds upon the OSATE2 environment for AADL.

Learn more:

Consistency of System Models

A cyber-physical system is a complex structure of its software,hardware, and physical elements, including their connections, relations, and properties. Representation and analysis of all these elements is carried out with models of different kind. An example of such a system (a quadrotor) and its models are shown in the image to the right. In CPS, a set of differential equations may describe the behavior of a physical system; a Simulink model may describe the controller; and a finite state machine may model software processes.

One obstacle to sound and efficient design and verification of CPS is the profound heterogeneity of models: their notions of computation, time, and state may be very different. This situation brings about the problem of consistency: how can we demonstrate that models do not have conflicting assumptions about the system structure and behavior? Is it possible to compose a correct system from heterogeneous models? How to avoid the communication breakdowns between the designers of different models?

My research focuses on creating a CPS multi-view framework that facilitates creating and maintaining inter-model relationships. I use architectural views to abstract crucial aspects of models and relate them to each other. Given this connection, we create algorithms to check and repair consistency of models via consistency of each model's view.

Learn more:

  • For a summary of our approach to CPS model consistency, see this paper.
  • For more detail on view consistency, see Ajinkya's thesis.

Projects

Journal Papers

Conference Papers

Workshop Papers