In real-world spacecraft systems, concurrent system activities must be constrained for energy efficiency and functional reasons. Such constraints must be considered in the early design phases, in order to avoid costly reiterations and modifications of the proposed system design in later phases. Although some initial attempts for using formal specifications exist in the domain, there is a lack of concurrency support in the utilized approaches. In this paper, we therefore first formalize an existing domain-specific language for specifying spacecraft designs and their constraints. Since this language does not support the modelling of concurrency issues, we extend it accordingly and map it to standard timed automata, based on a general system model. The new-style specifications can now be processed with existing and proven automata modelling tools, which enables faster and more reliable feasibility checks for early spacecraft system designs.
The model-based engineering paradigm is widely accepted in the aerospace industry.
One specific implementation is "Concurrent Engineering (CE)", an approach that has
evolved into an important support mechanism for early space mission design decisions.
It is supposed to clarify the baseline requirements and design properties for a future
spacecraft, such as overall mass, power consumption and costs for development and
operation. Studies have shown that up to 85% of the overall spacecraft project costs
result from decisions made in this early phase [
During the CE project phase, multiple spacecraft design alternatives are
simultaneously created, refined and analyzed by a group of engineers. Everybody in this group
has an own range of responsibilities, such as the consideration of satellite trajectories,
the realization of communication mechanisms, or the consideration of thermal aspects
[
The following paper discusses the consideration of concurrency demands and restrictions in the CE project phase based on a formal specification. Section 2 first introduces an abstract system model for spacecraft systems, in order to restrict the model entities to a necessary minimum. Section 3 then explains a domain-specific language being used in a German spacecraft project for the formulation of constraints and properties. In Section 4, we show how this DSL must be enhanced to consider concurrency issues properly. Section 5 finally explains how the resulting DSL can be translated to timed automata for better analysis support from existing tools. 2
A spacecraft system can be modeled as a set of internal and external state variables S = IS ∪ ES. The internal state si is defined by all state variables that can be directly manipulated through spacecraft’s activities, e.g., the charging level of the battery or the available free memory. External state variables change by themselves and are not directly affected by spacecraft activities. Examples are temperature, the time, or the availability of sun light. They constitute the external state se.
The spacecraft activity can be abstractly defined based on the idea of interacting components. One relevant property here is the consideration of their concurrent activities and their relation to time. Let T = {τ1, ..., τn}, n ∈ N be a set of operational states representing activities of the spacecraft components, e.g. the active charging of the satellite battery from solar panels or the usage of some data transmission down-link. I.e., for each τi, there exists a transition function fi(se, si, Δt) = Δsi that describes the change of the internal system’s state if a component is active for the time Δt.
In real-world satellite systems, concurrent component activities must be constrained for energy efficiency and functional reasons. Not all spacecraft components can be active at the same time. Let C = {c1, ..., ck}, k ∈ N represent a set of constraints for the state variables. Please note that the mission goals can be seen as special mission constraints.
Given the above definitions, a schedule or a plan is defined as a mapping of the component activity set T onto a set of time intervals:
P : T 7→ I, (1) where I = {(b, f ) : b, f ∈ R+, b < f } is a set of finite length time intervals with b, f begin the start- and end-times of the intervals, respectively. As a side condition, all Ci must be true at any time.
Based on the given system model, we are now discussing how constraints can be formulated and checked for a specific system model instance. 3
Different methods can be used to check a spacecraft system model’s compliance with
the intended constraints and goals for the planned mission time. Schaus et al. described
how an expert can formulate such requirements in a dedicated domain specific language
(DSL) and use search algorithms to check the feasibility with respect to the given
constraints [
Originally, the proposed concept was called continuous verification. We avoid the term ‘verification’ intentionally here, since at such an early design phase there is no real detailed system specification against which the system would be formally verified. Actually, creating unambiguous specifications is the purpose of the whole preliminary analysis. Instead of ‘verification’, the terms ‘feasibility study/check’ will be used.
In the published DSL syntax, the engineer can define different system components being exclusively active (called states) and system parameters (called operational state variables) which can be changed by the components’ activities. The values of these parameters define the global system state. I.e., there exist implicit constraints ∀i, j, i 6= j, τi ⇒ ¬τj (2)
The mission goal is defined as a constraint on the operational state variables. Additional constraints beside the central mission goal can also be formulated. Furthermore, for every component there are corresponding rates of changes to the system parameters. The generated mission plan is a chain of activity periods derived from this description, such as Battery Charge → Collect Data with Cameras → Send Data to Earth → Idle → ....
Since satellite systems depend not only on the internal components, but also on the
execution environment, there is a possibility to describe such environmental properties
in the DSL, too. This is done by parameterizing external simulation models (SGP4) [
The original DSL from [
Since in the original language there is no component concurrency being considered, only one component resp. operational state can be active at any point in time. Consequently, there is no explicit time notion in the language, with the only exception of simulation step which is the parameter fed to the external orbit simulator. This also determines the values for the changes of state parameters and the maximum number of steps before the mission deadline.
An important issue in the aforementioned DSL is that the operational state of the system, a vector of all state variables, is assumed to be directly bounded to the state of the currently active component. In other words: The system is specified with having only one active component at a time. This is an obvious over-constraining of the model, since a satellite as a system cannot be observed isolated from its environment. Concurrency consideration should be therefore not only a possible, but a desirable property. Several components of a satellite can be active simultaneously. One simple example is data being sent to earth while the battery is being charged. Furthermore, such a restrictive execution model can lead to the false negative check result, although the mission could still be possible to execute with a more “dense” plan1.
Supporting concurrency in the DSL and the implied execution model would lead to increased expressiveness of the language and allow for more realistic derivable analysis results. Furthermore, with the concurrent execution model the generated plans are more ‘dense’ and thus the probability of a false negative result of the feasibility checking is lower. 4
Given the formal system model from Section 2, we translate the semantics of the given DSL first into the set-theoretical constructs to understand the missing expressivity and determine the necessary enhancements: – A solver is implementation-specific and defines a search method to trace the state space of a given problem. Hence, it is not part of the formal model. – The state parameters are represented by the set S of state variables in the formal model. Their initial values are implementation-specific. – The operational states are defined by the set T of the formal model. Starting State does not need to be determined by the engineer since a satellite can have several active components simultaneously and their enabling depends on the validity conditions. – The operational state changes are also defined by the set T of the formal model. – The operational goals and constraints are represented by the set C of the formal model.
There is no explicit notion of duration in the given DSL. The set of prohibited overlapped component activities is also missing in the explicit form. Implicitly, however, one could say that the set is given by the assumption in the execution model that all overlapped executions are forbidden. Furthermore, events which enable certain component activities are not explicitly present in the DSL. They are generated by the simulation modules and directly fed to the search algorithm. 1 Here, the term “plan density” is loosely coined to describe a possibility to use overlapping time intervals to pack more activity into the mission time.
For supporting the missing concurrency semantics, the DSL is now enhanced with three syntactical constructs, as shown in Figure 2: Explicit durations per component activity, prohibited component activity overlapping, and events + durations.
As a result of the reformulation and enhancement of the DSL grammar, the problem
of feasibility analysis can now be reformulated as an off-line scheduling problem with
several constraints [
We decided to map the enhanced DSL to Timed Automata [
Although hybrid automata are more general and more expressive than timed
automata [
Mapping the enhanced DSL to timed automata constructs enables the system modeler to generate mission plans with appropriate existing tools, based on a transformed description with the DSL. Generally, the following definition holds: Definition 1. A timed automaton A is a tuple (L, l0, X, Inv, T, Σ) where: – L is a finite set of states (locations) – l0 is the initial state – X is a finite set of synchronously running real-valued clocks – T ⊆ L × C(X) × Σ × 2X × L is a finite set of transitions l −g−,a−,→r l′, where g is the guarding condition for the transition, a is the action and r is a set of clocks which are reset by the transition – Inv : L → C<(X) represents an invariant for every corresponding location – Σ is an alphabet of all possible actions.
Timed automata can model communication through binary synchronization,
represented here by synchronization actions that are represented by according transitions.
They can be either input actions (sync?) or output actions (sync!) that are performed in
pair. [
In the sequential execution model of the original DSL, only one operational state was allows to be active at a time. Hence, in such a representation, the whole set of components can be modeled as a single automaton with single inactive state (for idle mode) and several active states - one for each component. The values of system parameters will change with the given rates in some finite fixed step size which will be measured by a global clock.
Mapping the enhanced DSL description to the timed automata formalism is now straightforward. An operational state or component activity can be represented by a single automaton consisting of two locations - Active and Inactive. Validity conditions for the component to become active are represented by guards in the language of the TA. Clocks represent a maximum duration, if any is given. A component can remain active or inactive so long as the invariants are correspondingly fulfilled.
Mission goals and constraints can be embedded in two ways. Constraints are simply the guards on the transitions or location invariants which cannot be violated. To each goal there exists a dedicated automaton which also consists of two states. Once the goal is reached this automaton moves from one location to the the second and remains there representing a fulfilled goal. If all of the goals are satisfied before the global clock reaches some predefined value (mission time constraints), then the mission is feasible. 5.2
Based on the original DSL expressiveness, [
Using the proposed enhanced DSL and its mapping to an automata formalism, the
TET-1 mission was again modelled by the authors in the UPPAAL tool [
We investigated a major improvement of the analysis run-time in comparison to the
original behavior, which is shown in Table 1. Feasibility check times are now in the
sub-second area. In comparison to the sequential methods used in [