Research Project
The Proteus Programming Language
(Design and Development of a Domain-Specific Language (DSL) Based on Hierarchical State Machines (HSM) for Model-Based Programming (MBP))
Lead Researcher
- Kyle Dewey, Computer Science
Collaborators
- Dr. Klaus Havelund: primary JPL contact, and directly involved in the work
- Dr. Michel Ingham: secondary JPL contact serving primarily in an advisory role
Student Team
- Morgan Barrett, Computer Science*
- Ahmed Bahyal, Computer Science*
- Deekshith Myakala Computer Science*
- Isaiah Martinez, Computer Science*
- Nicholas Rodriguez Weda, Computer Science*
- 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
Note: names marked with an asterisk (*) indicate current students
Funding
- Funding Organization: NASA
- Funding Program: MIRO
SYNOPSIS
- Hierarchical State Machines (HSMs) are used for the simulation of software models to be implemented, such as flight software and control systems
- In space applications, software correctness is top priority
- Existing languages developed have significant issues with one or more or usability, performance, and safety, making them problematic for HSM development
- Proteus allows for the definition of large systems composed of multiple asynchronously-communicating HSMs
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.
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
-
Model-Based Programming (MBP) Domain-Specific Languages (DSLs) allow system engineers to model and simultaneously implement system behavior
-
MBP DSLs also allow engineers to specify behavior and arbitrary constraints specific to the machine
-
Design in a way that is usable and approachable for JPL software
engineers -
HSM modeling and tracing are built into the language for ease of development
-
Goal: make a reliable language with built-in HSM support tha tfits seamlessly into JPL’s existing development toolchains
Research Methods
-
Designed to look and feel similar to C/C++
-
HSM support built directly into the language
-
Permits complex HSM design
Research Deliverables and Products
-
Demonstrated reliable HSM support
-
Multiple HSMs able to communicate with each other
-
Visible state execution trace
-
Eliminated issues with machine dependency
Commercialization and/or Societal Impact Opportunities
-
Applications: Embedded Programming
-
Key Values: Safe, fast, reliable, fault-tolerant
-
Potential Customers: Aerospace agencies, consumer electronics, medical device development
Research Timeline
Start Date: January – May 2020
End Date:
Lead Researcher
- Kyle Dewey, Computer Science
Collaborators
- Dr. Klaus Havelund: primary JPL contact, and directly involved in the work
- Dr. Michel Ingham: secondary JPL contact serving primarily in an advisory role
Student Team
- Morgan Barrett, Computer Science*
- Ahmed Bahyal, Computer Science*
- Deekshith Myakala Computer Science*
- Isaiah Martinez, Computer Science*
- Nicholas Rodriguez Weda, Computer Science*
- 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
Note: names marked with an asterisk (*) indicate current students
Funding
- Funding Organization: NASA
- Funding Program: MIRO
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