Research Overview

My overall research objective is to develop model-based methodologies, algorithms, and software tools based on a correct-by-construction approach. The aim is to enable engineering of complex systems in less time, with higher confidence in correctness. By correct-by-construction we mean that designers should be able to define their problem declaratively as formal models, which can be simulated, analyzed, and automatically synthesized into correctly working software systems. That is, the designers describe what the system should do, not exactly how it is executed. See the figure to the right for an overview of the main concepts of model-based correct-by-construction design (click on the image to enlarge).

The research can be divided into three main research areas:

These three areas are presented below. Besides the technical research, I have also been involved in pedagogical research. See for instance our work on the company approach to software engineering projects [IEEE TE'12], and assessment models for large project courses [SIGCSE'14].
Research Area 1: Modeling Language Research
We investigate formalisms and formal language semantics for describing various heterogeneous models of computations in the form of domain-specific languages (DSLs). Some of the main research topics are:
  • Embedding Domain-Specific Languages (DSLs). Our aim is to develop theory and software of expressive and analyzable host languages for embedding domain-specific modeling languages. Our main research effort is on Modelyze, a gradually typed host language for modeling and analyzing cyber-physical systems. See [PADL'12, EECS report'12]

  • Hybrid Co-Simulation. The main focus is on formalizing hybrid co-simulation semantics for the Functional Mock-up Interface (FMI) See: [EMSOFT'13, HSCC'15]

  • EOO Modeling Semantics. We develop static and dynamic semantics for equation-based object-oriented (EOO) modeling languages. I have been part of the Modelica language design group since 2005. Some results and contributions are on types [Modelica'06, GPCE'06], higher-order models [SNE'09], and some involvement in the open source tool OpenModelica.

  • Model-Based Machine Learning. This is a rather new initiative, where our aim is to apply our previous experience on equation-based modeling languages to the domain of machine learning. Our current work so far on machine learning has been focused on supervised and unsupervised learning methods in the context of software engineering and automated bug assignment. See [ESE'15] and [ArXiv'15].

Research Area 2: Time-aware Programming Language Research
The second research area concerns programming with time, meaning that real-time programming primitives are inherent parts of low level programming languages, such as C. The programmer declaratively incorporates timing constraints in the programming code. It is then the task of the compiler and the run-time system to guarantee that the timing specifications are fulfilled. Some of the main research topics are:
  • Time-aware Programming Constructs. We investigate different programming constructs for expressing time, time stamping, and timing constraints in low-level programming languages. This work is part of an international effort called Time-Aware Applications, Computers, and Communication Systems (TAACCS). See www.taaccs.org and this NIST report. See also our work on relaxing the synchronous programming approach for mixed-criticality systems [RTAS'14].

  • Timing analysis and Verification. The challenge concerns formal verification of specified timing constraint. Such verification requires a sound timing model of the hardware and software system that are being analyzed. See our work on interactive timing analysis [RTNS'16], WCET-Aware dynamic code management on scratchpads [RTAS'14], and approximate synchrony, a modeling and verification approach for almost synchronized systems [CAV'15].

Research Area 3: Predictable Systems Research
We are interested in developing software and hardware systems that are more predictable. The research is focused on architectures and protocols that are targeted for distributed and mixed-criticality systems. Some of the main research topics are:
  • Precision Timed (PRET) Machines. This work has been developed during my time at UC Berkeley, in collaboration with students and researchers in Edward Lee's Ptolemy group. The main idea is to perform real-time scheduling in hardware instead of software, to achieve more timing predictable systems. An early ARM-based prototype called PTARM was developed by Liu et al. [ICCD'12], which was limited to fixed number of hardware threads. Later, we developed a more refined design call FlexPRET, which can dynamically allocate hardware threads and is designed for mixed-criticality systems [RTAS'14]. You can also get an overview of the vision and challenges of a PRET infrastructure in this paper [ESLsyn'13].

  • Predictable Memory. We have also developed techniques for predictable memory systems. In particular, see our work on a predictable DRAM controller for mixed-criticality systems [RTAS'15].

  • Clock Synchronization. As part of the TAACCS initiative, we are also interested in the development of methods for time sycnhronization in distributed systems. See our study of the IEEE 1588-2008 clock synchronization protocol [ISPCS'14] or our review article on temporal issues in cyber-physical systems [JIIS'13].


This is a personal web page. More information.