Research Project

Design and Development of a Domain-Specific Language (DSL) Based on Hierarchical State Machines (HSM) for Model-Based Programming (MBP)

Motivation/Research Problem
Hierarchical state machines (HSMs) form the basis of Model-Based Programming (MBP – http://groups.csail.mit.edu/mers/papers/CP177.pdf), which is usually accomplished via domain-specific languages (DSLs).  MBP DSLs allow systems engineers to model and simultaneously implement system behavior.  Ideally, MBP DSLs also allow systems engineers to specify arbitrary constraints on the system, and the language will verify that these constraints hold; for example, systems engineers can use MBP DSLs to prove that their system works correctly.
Research Team

Collaborators 

  • Klaus Havelund: primary JPL contact, and directly involved in the work
  • Michel Ingham: secondary JPL contact serving primarily in an advisory role

Faculty 

  • Kyle Dewey – Computer Science

Student Team

  • Arian Dehghani
  • Rebecca Carbone
  • Kennedy Ashley Johnson
  • Sherinne Kylie Ramos
  • Oluwaseetofunmi Komolafe
  • Brian McClelland
  • Andrew Nathensond
  • Marcello San Augustin
  • Kate Go
  • Alice Balayan

New students:

  • Arian Dehghani, Rebecca Carbone, Kennedy Ashley Johnson, Sherinne Kylie Ramos, Oluwaseetofunmi Komolafe, Andrew Nathenson, and Marcello San Augustin

Students no longer involved:

  • Meyer Millman, Daniel Tellier, and Michael Munje

Students involved only during Summer 2020:

  • Eileen Quiroz, Frank Serdenia, and Simran Gill
Alignment, Engagement and Contributions to the priorities of NASA’s Mission Directorates
JPL is interested in MBP DSLs, and has purpose-built two of them: ScalaHSM and TextHSM.  However, both of these languages are lacking.  For our purposes, we will discuss these in terms of two important criteria: usability (how easy the language is to use, particularly for common systems engineering tasks) and safety (what can be verified correct, and what sort of behavioral guarantees are provided).  ScalaHSM is not particularly usable, as it requires systems engineers to already be familiar with the Scala programming languages; most systems engineers are unfamiliar with Scala, and Scala has a steep learning curve, making ScalaHSM impractical for its target audience.  In contrast, TextHSM assumes only prior C knowledge, making it more accessible for systems engineers.  However, TextHSM does not provide any capabilities to reason about what this C code does; indeed, it just blindly assumes the C is correct.  As such, TextHSM is unsafe to use.
Research Questions
  • We are guided by one overarching question: how do we combine the best of usability and safety into a single MBP DSL?
Research Objectives
This is more complex than simply combining ScalaHSM and TextHSM; whole languages cannot be composed in this manner. Additionally, we want to move beyond the current safety guarantees of ScalaHSM and allow users to write much more complex properties which are checked at compile time.

Towards answering this question, we wish to develop a new MBP DSL named Proteus, which is both usable and safe. Notably, Proteus will:

  • Be usable by systems engineers. Unlike ScalaHSM, it will not assume familiar with languages outside of the typical set known by systems engineers.
  • Allow for strong static guarantees and enable reasoning about HSM behavior, surpassing both TextHSM and ScalaHSM.
  • Compile to C/C++, which are appropriate for real-time systems. This will also allow Proteus to work with existing embedded development pipelines.
Research Methods
To ensure that Proteus is usable by, and useful for, systems engineers, we will solicit feedback from key stakeholders (e.g., JPL system engineers, software scientists) regarding major language features and trade-off considerations (e.g., compile time, ease of writing specifications, ease and expressiveness of verification). As part of this process, we will also gather use cases for Proteus, as well as existing uses of ScalaHSM and TextHSM. These use cases and existing uses will serve as a benchmark suite with which to evaluate Proteus.

Proteus will be developed using modern compiler design and implementation approaches, being sure to use existing components (e.g., parser combinators for parsing) where possible. It will be architected as an interaction between a lexer, parser, typechecker/verifier, and code generator. To minimize the time before we have a working prototype, we will implement Proteus incrementally; we will first isolate a minimal, highly restricted feature set, and implement that. From there, we plan to grow the language via the addition of features. Not only does this minimize the time before we have a product, it also gives something complete enough so that stakeholders can provide feedback on its design in early stages.

For each version of Proteus, we will implement the aforementioned benchmarks, and use this as a way to gauge Proteus’ usability and safety. This will also enable us to measure the performance of the language (both compile time and run time), and to test the language on realistic scenarios.

Research Deliverables and Products

Deliverables listed in last reflective journal:

  • A list of features of interest identified by key stakeholders
  • The Proteus compiler, including example usage and documentation
  • Use cases derived from ScalaHSM and TextHSM implemented in Proteus, along with the results of their application on Proteus relative to ScalaHSM and TextHSM
  • Next steps for extending Proteus

To date, we have implemented a complete executable prototype of Proteus, including a lexer/tokenizer, parser, typechecker, and code generator. Some basic documentation and examples have also been produced, as well as a list of major features we’d like to add which was produced in collaboration with JPL stakeholders. With this in mind, we’ve produced all the deliverables except for 3 (use cases implemented in Proteus); there have been unexpected delays in getting access to these use cases. However, this hasn’t slowed us down, and we are still extended Proteus. Reflecting Proteus’ current state, the following deliverables are planned for the future:

  • Use cases derived from ScalaHSM and TextHSM implemented in Proteus, along with the results of their application on Proteus relative to ScalaHSM and TextHSM (carry-over of 3 from before)
  • A built-in system for runtime fault monitoring and response, which is to handle faults which either cannot be, or cannot easily be, statically prevented
  • Support for typeclasses
  • Support for basic data structures
  • Next steps for extending Proteus (a perpetual process, carried over from the last time)

Publications

Ideally, this work should be published (and seems publishable based on prior reading), though we have not yet discussed appropriate venues. Klaus has extensive experience getting work like this published, and likely has a list of appropriate venues.
Conference Presentations

We submitted a conference paper to AIAA ASCEND which was accepted. However, it was unfortunately later withdrawn as Meyer Millman unexpectedly did not present it; we’ve been unable to get in contact with Meyer, but we know he’s ok.

Research Timeline
January – May 2020 (lead: Brian McClelland) —

  • Add fault monitoring capabilities to Proteus
  • Demonstrate these fault monitoring capabilities work, using non-trivial examples
  • Improve test suite quality to build further confidence that these new capabilities work

January – May 2020 (lead: Kyle Dewey and any volunteers) —

  • Continue work to get access to example HSMs from real environment
  • Try to implement these HSMs in Proteus, record pain points where implementation is difficult or impossible, and use this information to iterate on Proteus’ design
  • Discuss our observations with JPL stakeholders to prioritize and further refine planned improvements

January – May 2020 (lead: Andrew Nathenson) —

  • Add support for basic data structures
  • Implement a variety of tests involving basic data structures to ensure they work as expected

January – May 2020 (leads: Kate Go, Alice Balayan, Arian Dehghani) —

  • Finish adding support for typeclasses
  • Implement related tests to ensure they work properly
  • Depending on when Andrew’s contribution is finished, ensure they work with basic data structures

May – August 2020 (lead: Kyle Dewey and any volunteers) —

  • Investigate appropriate venues for publication
  • Update prior AIAA conference submission to reflect Proteus’ current state
  • Polish the submission to get it to be ready for peer-review, particularly by augmenting it with an evaluation demonstrating Proteus’ capabilities over prior systems it is intended to replace.
Are there other current and planned ARCS related projects?
I am a Co-PI with Joe Bautista and Li Liu on a NASA STTR for visualizing HSMs, which was funded. Once a visualization is complete, we plan to integrate it into Proteus, and use it instead of Proteus’ current text-based representation. This will involve collaborating with other students in ARCS and will likely require recruiting new students who are not already affiliated with ARCS. The work itself could potentially be conducted as a senior design project, depending on what we determine the scope and complexity to be.

I was originally planning to submit a related NSF CRII grant in August 2020, and I completed most of the related materials. However, due to COVID, the deadline was extended to November 2020 fairly late. This unexpected change was actually problematic – one is only eligible for the CRII in the first three years of their academic career, and this change was enough to push me past the three year mark. I confirmed with the program manager that was no longer eligible. I was also planning to submit a NASA STTR in March 2021, though the deadline was unexpectedly changed to early January 2021, which did not leave me sufficient time to get the grant together. I am still hoping to submit for the NASA Early Career grant in April.

Impact of Project Partnership with NASA:

Klaus Havelund and Michel Ingham have continued to be excellent collaborators. They have exposed me to a variety of wide-open research areas, and most of my current research program is based around their ideas. A significant part of my research now involves programming language design and development, which exploits a significant amount of Ph.D. training I received which formerly was underutilized.

Additionally, the name recognition and prestige associated with NASA and JPL is not lost on students. I have had a steady pipeline of incoming interested students who are attracted to working with such big names. This has been an effective recruitment tool.

Overall, there has been more growth to my research than I anticipated, both in terms of the number of students involved, as well as related projects, grants, publications, and collaborations. I’ve found that I needed to scale back a bit in order to avoid stretching myself too thin, particularly with significant increases in the rest of my workload due to COVID. My collaborators have been understanding of this.