Software faults are the causes for repeating catastrophes in modern space missions. There are various problems in lifecycle of flight control software including lack of adequate models of real-time control algorithms. Real-time control algorithms have the totally distinct nature in contrast to computational algorithms. The paper presents mathematical models suitable for analysis, design and formal verification phases of lifecycle of spacecraft's flight control software. Two kinds of models - graph-based and algebraic, are being described. These models were successfully introduced in computer aided software engineering toolset for design and verification of spacecraft's real-time onboard control software.
The modern spacecraft usually has various onboard systems such as Energy Supply System, Motion Control System, Onboard Control System, Autonomous Navigation System, Telemetry System, Thermal Control System, etc. In turn, each onboard system consists of a set of devices, aggregates, sensors. We can state that spacecraft is a system of systems or complex of complexes. Functioning of all these devices should be coordinated both in time and logically. The real-time mode of functioning is a very important issue entailing more complex nature of required models to be used for adequate reflecting of features of onboard apparatuses. This aspect is also quite important when we deal with the problems connected with designing and implementation of dependable control system for the spacecraft. In accordance with the Ashby’s Law of Requisite Variety, variety of onboard equipment’s behavior requires variety of onboard control system. Today the control logic of onboard control system is implemented in onboard Flight Control Software. Roughly speaking, there is a special control software module for each onboard device or aggregate. There are also a lot of supplemental modules involved into organization of computational process, etc. This is an illustration to a structural aspect of complexity of modern spacecraft’s onboard software. Another essential aspect corresponds to behavioral aspect of complexity. We can compare the onboard apparatus of the spacecraft with the orchestra with the string and wind instruments, drums, etc. But we need a conductor to get a symphony – violin should start at the right moment, next cello should start with accurately fulfilled delay, and so on. So, we need also a special sort of real-time software which will serve as an orchestra’s conductor.
For example, there are about 500 software modules concurrently running at real-time mode onboard the modern spacecrafts
manufactured by Samara Rocket and Space Center ‘Progress’ [
What is a reason for it? Complexity of onboard equipment entails failures of devices (which can be parried by switching to reserve equipment executed by special software module, but it requires more complex control logic). Complexity of the spacecraft tasks entails more complex behavior (especially in abnormal situations). Complex behavior also requires complex control logic. Complex Control Logic entails ‘broken phone effect’ between onboard devices’ specialists and programmers during coding it in Onboard Flight Control Software. Nowadays, complex control logic requires complexity of Flight Control Software. Complexity of Software means higher costs of software lifecycle. Moreover, complexity of software means more errors in software itself. Is it a vicious circle?
Summarizing, we can emphasize the following modern trends and problems in spacecraft control: 1. use of onboard computers as a main control system;
Mathematical Modeling / A. Tyugashev
2. transfer of ‘decision-making point’ from Earth onboard;
3. growing of size and complexity of Flight Control Software (concurrent multi-tasking, hundreds of interacting modules,
millions of lines of code);
4. software-based support of spacecraft’s fault tolerance feature;
5. dozens of people including non-programmers, involved in lifecycle of Flight Control Software;
6. costs of Flight Control Software’s lifecycle became a very significant part of space mission’s total costs, moreover
design, development and testing of the Onboard Software often is a ‘critical path’ in network schedule of spacecraft ‘s
producing as a whole;
7. labor costs of control system software’s creation and testing is 10 times bigger than hardware related costs [
The very promising way in this area is application of formal verification methods [
The object of the study is real-time control algorithms. It should provide coordinated and well synchronized functioning of onboard spacecraft’s systems containing various sensors, actuators, devices.
The very important features distinguishing the control algorithms from the data transformation algorithms are the following. First, we cannot correlate the function (in mathematical understanding), and the control algorithm. Moreover, the correctness of the control algorithm cannot be defined by the contents of the computer memory at the moment of algorithm’s end. The correctness of the control algorithm depends on its behavior in full time interval of functioning. Moreover, the values of conditions during execution of data transforming program are totally defined by the input data while the values of the conditions to be considered in control algorithm, are unpredictable because they are formed by the parameters of physical processes in controlled object (for example, velocity of the spacecraft). Actions executed by the control algorithm also can change not only the data in memory of the onboard computer, but influence on the state of the controlled object. When we need, for example, land the spacecraft on the Mars, we need to implement the very complex sequence of the operations with the participation of various onboard devices and mechanisms – but all of them are under control of onboard software.
Unfortunately, the major efforts in the modeling of algorithms historically were focused on data transformers, since earliest models like Turing and Post Machines, Church’s recursive functions and Markov’s ‘normal algoriphmes’. But if we want to apply the promising modern methods like formal verification or automated synthesis of the control software with the guarantee of its properness, we need the adequate semantic model for the control algorithm.
We can describe the following features of ‘traditional’ computational programs. Their main goal is transformation of input
data to output data. The main components are the data transformers. The computational program correct if it successfully
finishes (if input data is right) meanwhile output data matches specification. Structure of the traditional step-by-step sequential
computational algorithm can adequately be represented by flowchart with begin and end(s) nodes. There are no time constraints
and timer(s). Semantics could be adequately formalized by
1. axiomatic semantics [
Many control algorithms are being used by ‘reactive’ systems. The main features of such systems could be described as
follows. The reactive system should right process the input event flow. The main components are actions (in contrast to
computational algorithms). The following semantic models are used for reactive systems:
1. Kripke structures [
Other important features of algorithms used in reactive systems distinguishing them both from the traditional programs and real-time control systems: 1. there are no end of algorithms, use of infinite loop of event processing instead; 2. there are no time constraints and time scale (timers) - asynchronous nature; 3. correct, if algorithm implements required model and execute right actions as reaction on pre-defined events.
We deal with Time-Driven Real-Time Control Algorithms (RTCA). This kind of algorithms has very important distinguishes from the reactive systems. Time-Driven Real-Time Algorithm should implement required schedule(s) (the term ‘cyclogramme’ widely used in space industry). The main components of algorithm are actions.
Other essential features can be described as follows. There are begin and ends in contrast to reactive systems. There are ‘hard’ time constraints. There is time scale (timers) for quantitative description of time parameters. In other words, RTCA has a
Mathematical Modeling / A. Tyugashev synchronous nature. This kind of algorithm correct if it execute right actions at right time (more precisely, right time mome nts with right considering of the current situation). Thus, the adequate semantic models should consider the stated features.
The known semantic models are
1. timed automata [
These models are based on the idea of ‘state’. Unfortunately, if we try to apply this approach to real world system, we suffer because of ‘state explosion’ problem. This is why the author try to develop and use in CASE toolset another model based on idea of process. In some vision, this model utilizes more high level of abstraction allowing avoiding undue detalization and using in practice.
As it presented in [
Each i-th quad in the above set describes one action executed by the real-time control algorithm; N is a number of actions executed. Here fi is an identifier of the action, ti – starting time of the action, i - duration. Starting time and duration defined as integers, this is adequate time model in this case because the minimal time difference recognized by the control algorithm is a ‘tick’ of onboard clock generator. The set of elementary actions F should be previously defined, fi ϵ F. Logical vector li specifies the combination of the conditions, allowing action fi to be executed in time interval [ti; ti + i]. For example, logical vector can looks as follows ([1=1], [2=H],…[M=0]). The 1 and 0 values recognized as true and false, and the third value ‘H’ means that this condition does not have an impact to execution of the action at specified time. The number of conditions actual for the control algorithm as well as the set L of the condition itself should be settled simultaneously with the set F of actions. We can interpret the logical vector in the model as an analog of the well known ‘guard’ conditions.
Described model have a very clear and intuitive visual representation looks like Gantt diagram. This was a reason because
this model and models inherited from it were intended to use and successfully applied during development of the
GRAFKONT/GEOZ [
But the ‘basic’ algebra of the control algorithms had the restricted descriptive power, for instance, there was no possibility to specify arbitrary time intervals between the actions, so it was necessary to introduce ‘fictive’ actions to taking in account the delays. And the time had the ‘relative’ nature only; we had no mechanism for binding the actions to the particular moment.
There are some known models for parallel systems utilizing higher level of abstraction than state-based models. First of all,
we should mention the following approaches:
1. process Algebras (Milner’s CCS [
Unfortunately, there are serious limitations for use of named models for Flight Control Software. If we talk about process algebras, we should underline the following. They provide just ‘common’ means for description of parallel execution of processes without opportunity to define coordination of processes’ begins and ends. Process algebras do not support logical inference (reasoning about algorithms needed for verification purposes). And there are no any tools for description of various situations (conditioning for different variants of situations – regular, abnormal, emergency, etc.) of system’s functioning. But in space missions we definitely need such instruments.
In contrast to process algebras, temporal logics natively have special means for description of concurrency of processes extended in time. But initially, there are no means for quantitative aspects of synchronization in temporal logics. In addition, the semantic models are not advanced enough for our practical purposes.
Allen’s Interval Logic is a very interesting and promising approach providing means for description of all possible overlay of processes extended in time. But there are no means in Allen’s logic for description of quantitative aspects of synchronization. Moreover, this approach also has no means for description of ‘different branches’ of Real-Time Control Algorithms.
The method we developed is free from the limitations described above. It was initially developed for description of complex Real-Time Control Algorithms with considering internal logic, different variants (branches) and situations. There are advanced means for description of synchronization of parallel processes. There are means for quantitative descriptions of synchronization both for relative and absolute timing.
The proposed model uses ‘constructive’ approach. We can construct new control algorithms using the existing ones by application of the set of operations. The basic operations introduced by Anatoly Kalentyev had only four operations – CH, СК, →, and . The extended algebraic model contains the following operations:
Anyway, if we want to solve the synthesis problem of the program, we need the adequate model with the more deep detailing.
The model in previous section specifies the control algorithm at the ‘semantic’ level. We can see parallel with the denotational semantics of the data transformation algorithms when we nominate the function to be calculated by the program. But the same semantics can be provided by different implementations. Moreover, it is well known fact that in case of software, the quality and characteristics – including efficiency, of the programs with the same semantics, can be quite different.
We need the models for the next degree of detalization. The very popular and effective in practice models in theoretical computer science are graph-based. They are applicable also at the stages of design and analysis of efficiency of implementation of flight control software as well. However, the known models require clarification and extension.
For example, the control flow graph is a very useful and popular model. But initially it describes sequential imperative program executed by the single CPU. Understandably, there are no any essences applicable for describing phenomena of time interval.
But the nature of the complex technical system likes modern spacecraft urgently requires concurrent (multi-tasking) model of computation. It is unsurprising that the onboard software of the modern spacecraft is executed by the control of multi-tasking operating system. Such systems have an application programming interface allowing one process to be started by another (fork). In many cases, onboard real-time operating system allows starting the process with the specified time delay or at absolute time.
This is the reason for defining the extended model – ‘timed logical scheme’ of the real-time control algorithm. First, we take the well known program control flow graph. In case of control algorithms, nodes with the single outgoing arcs will be associated with any actions executed by the algorithm. Nodes with the two outgoing arcs will be associated with the conditions formed not by the CPU flags only, but related to parameters of spacecraft motion, state of the onboard systems, etc.
Mathematical Modeling / A. Tyugashev
We introduce also the special ‘weighted’ arcs. The weight specified by the integer, will denote the delay before the action associated with the following node be executed. The very important issue is that any ‘action’ node can have arbitrary number of outgoing ‘weighted’ arcs additionally to one ‘usual’ unweighted. The example of the timed logical scheme is presented in Figure 1 in alongside with the visual representation of the corresponding semantic model of control algorithm.
The depicted UA is {<f1,0,20,(1=1)>, <f2,0,100,(1=0)>, <f3,20,200,(1=1)>, <f4,180,50,(1=H)>, <f5,220,15,(1=Н)>}. Different qualification by the logical vectors can be shown by different texture or color on visual representation of the control algorithm’s semantics. Timed logical scheme implements the semantic by the fixation of the ‘key’ time moments – 0, 20, 180, 200 when the algorithm must perform actions. This ‘activations’ are divided by relatively time delays: 20, 160, 40, 180 associated with the weighed arcs in the graph-based model. We can see the ‘qualified’ branches of the timed logical scheme with the corresponding (1=1) and (1=0) conditions (in this case, there is only the single condition in the logical vector). Then, at timestamp 180, these branches join again.
The presented models looks be much more adequate to the nature of the onboard spacecraft’s flight control software than approaches oriented to computational sequential algorithms. Nature of the presented models is quite corresponds to the domain of real-time control of technical complexes consisting of many subsystems, devices, aggregates, etc. The main components of control programs are actions which can be executed both by software modules and equipment. The conditions which influences the process of computation, also does not formed by the input data only, but permanently changing in accordance with the state of controlled object. The semantic model presented in the paper, initially oriented to this particularities.
These features provide possibility to potential application of these models in such area as SCADA systems, power plants,
transport, etc. [
If we compare presented timed logical scheme of the algorithm with the timed automaton, for example, we will discover that despite there are possibility to describe time related issues, timed automata cannot be used to adequate and unambiguous descriptions of control programs. Timed logical scheme, conversely, initially was developed with this purpose and good corresponds to the factors of problem domain. Moreover, the features of real-time operating systems are taken into account.
The paper presents two extended models for representation of real-time control algorithms implemented by spacecraft’s flight control software. One model is algebraic and another is graph-based. Algebraic model can be applied for ‘high level’ semantic modeling of the real-time control algorithms. This is important because known models were oriented to computational algorithms and did not take in account the nature of real-time control systems. Semantic models can be used for the accurate and unambiguous specification of flight control software and then applied for formal verification, which is reviewed nowadays as very promising method around the world.
Another presented model is graph-based. It allows analyze the efficiency issues and can be successfully used at the design stage. Constructive nature of these models and their clear visual representations allow developing of GRAFKONT/GEOZ software toolset for specifying and verification of real-time control software. The toolset was introduced at Samara Space Rocket Center.
Author should say many thanks and acknowledgements to President of the Samara University Victor Soifer who granted him a possibility to research and develop the methods and tools for Russian space industry for many years.