Research Project

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

Research Team

Lead Researcher

Kyle Dewey – Computer Science

Collaborators

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

Student Team

Alice Balayan*
Rebecca Carbone*
Arian Dehghani*
Simran Gill
Kate Go*
Kennedy Ashley Johnson*
Oluwaseetofunmi Komolafe*
Brian McClelland*
Meyer Millman
Michael Munje
Andrew Nathenson*
Sherinne Kylie Ramos*
Marcello San Augustin*
Eileen Quiroz
Frank Serdenia
Daniel Tellier

* Current Students

Funding

Funding Organization: NASA
Funding Program: MIRO

Abstract

In space and flight applications, hierarchical state machines (HSMs) are often used for writing simulation and control software, including that of the Curiosity rover. At the Jet Propulsion Lab (JPL), multiple programming languages have been developed specifically for writing HSM-based software, and these have been used in practice. However, we observe that the existing languages developed have significant issues with one or more of usability, performance, and safety, making them problematic for HSM-based development. To address these concerns, we are taking lessons learned from these languages and developing a new programming language named Proteus. Proteus builds HSM support directly into the language and permits complex HSMs to be defined that communicate with each other. Proteus is designed with a look and feel similar to C/C++, making it usable and approachable for JPL software engineers. Proteus itself compiles to C++, allowing it to fit easily into existing development toolchains, making it amenable to embedded real-time systems. To ensure that Proteus will be of use to its target audience, it is being iteratively developed through a series of prototypes that are regularly evaluated by key JPL stakeholders, ensuring Proteus always stays on track. While Proteus is still very young in its development, we demonstrate its basic viability with an example utilizing multiple independent HSMs communicating with each other and a relevant execution trace. In the future, we plan to apply Proteus to larger HSMs taken from real space applications, and many additional relevant features are planned.

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.

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 as 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 familiarity 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 is appropriate for real-time systems. This will also allow Proteus to work with existing embedded development pipelines.

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 familiarity 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 is 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

Internal to the project, we have already produced:

A list of features of interest identified by key stakeholders
The Proteus compiler, including example usage and documentation
Some existing HSM-based software ported to Proteus
Next steps for extending Proteus

From the last reflective journal, the following internal deliverables were planned:

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)

With #1, we changed the deliverable a bit to include any HSM-based software (instead of just ScalaHSM and TextHSM), which widens scope of what is relevant. We are actively working on this now, and have already ported some software from JPL. With #2, a runtime fault monitoring system has been completed and is part of Proteus. With #3 and #4, these portions are partially implemented, but incomplete. #3 and #4 need project leads, and #1 currently has higher priority. #5 is ongoing.

Publications

Since the last reflective journal, SMC-IT was identified as an appropriate peer-reviewed venue. Our prior AIAA ASCEND conference paper was reworked for SMC-IT, and was ultimately accepted. We are working on the camera-ready version of the SMC-IT paper now.

Presentations

Since the last reflective journal, there have been no conference presentations. A conference presentation is planned for SMC-IT, possibly by Brian McClelland. Some students who were previously on the project (Simran Gill, Eileen Quiroz, and Frank Serdenia) gave a presentation at the AIMS^2 Student Research Symposium regarding work they performed on Proteus during Summer 2020 (internal to CSUN). Additionally, Rebecca Carbone and Kennedy Johnson have presented on their Proteus work twice internal to ARCS, once during the ARCS seminar series and once with JPL stakeholders.

Other

Brian McClelland completed his MS thesis, which specifically concerned Proteus.

Research Timeline

Start Date: January – May 2020
End Date: