Artist's depiction of the Voyager spacecraft Credit: NASA / JPL

The NASA Voyager Mission was designed for exploration of the Solar System. The mission started in 1977, when the twin spacecraft Voyager I and Voyager II were launched. The original mission objectives were to explore the outer planets of the Solar System. As the Voyagers flew across the Solar System, they took pictures of planets and their satellites and performed close-up studies of Jupiter, Saturn, Uranus, and Neptune.
  After successfully accomplishing their initial mission, both Voyagers are now on an xtended mission, dubbed the Voyager Interstellar Mission. This mission is an attempt to chart the heliopause boundary, where the solar winds and solar magnetic fields meet the so-called interstellar medium. All this makes Voyager the most successful planetary exploration mission of all time.

The great success of the NASA Voyager Mission, designed and built over 30 years ago, and the fact that autonomous behavior persists in the Voyager requirements, make the same a good example for future space missions. Here, it is our understanding that both prototyping and formal modeling, which will aid in the design and implementation of future Voyager-like missions, are becoming increasingly necessary and important as the urgent need emerges for higher levels of assurance regarding correctness.
  Our long-term objectives are the modeling and implementation of autonomic system prototypes of future Voyager-like missions, thus allowing for benchmark experiments to compare prototyped autonomic features and issues with the actual Voyager Mission. To achieve these goals, we apply ASSL to build formal models and generate functional prototypes for the Voyager mission. The generated prototypes help us validate the features in question and perform further investigations based on practical results under simulated conditions. Note that knowledge of the Voyager Mission enables us to compare issues arising in the mission itself with potential approaches to their mitigation.
  Our first objective is to specify with ASSL and generate a prototype model for the image-processing behavior observed in the NASA Voyager mission. Note that while exploring the Solar System, the Voyagers were able to detect interesting objects and take pictures of the same on-the-fly. This reveals a form of autonomic event-driven behavior, which we specify with ASSL.

An autonomous-specific behavior is observed in the Voyager spacecraft when a picture must be taken and sent to Earth. In the course of this project, we specified the image-processing behavior of the NASA Voyager Mission and generated the AS (autonomic system ) prototype of the same with ASSL. We applied the ASSL multi-tier specification model to specify the Voyager II Mission as an AS composed of the Voyager II spacecraft and four antennas on Earth, all specified as distinct autonomic elements. Next, we generated the Java application skeleton for the prototype of the Voyager II Mission and experimented with it to explore important state-transition operations ongoing in the system at run-time and to trace the behavior of the generated system.
  One of the specification models developed in the course of this project and the generated Java code can be downloaded here:
  » ASSL Specification
  » ASSL-generated Code