Formal Data Validation of Flight Configuration Data
| Success Story|
|Keywords||Event-B, configuration data, validation|
Nowadays lot of critical systems used in aeronautic, aerospace, automotive and railway domains are designed to be highly configurable. In such systems, the data configuration validity is of tremendous importance. The railway domain does already apply formal techniques to validate configuration data. A study carried out by Systerel and funded by the CNES demonstrated the suitability of such methods for validation of flight software configuration data.
of Interest to Engineers and Analysts
- TOOL-EA-2 Are tools functionality automating all tedious tasks?
Comparing the approach based on a formal model with the previous approach based on specifically designed software (with hardcoded properties) has the following advantages:
- Mathematical notation is the best compromised between the human (expressing a property) and the machine (verifying the property)
- Reduced validation costs: the validation platform is generic while the old software must be validated for each system and even when a property is modified
- Better quality of the validation: ex. pointer types
- Better transparency: the domain expert can check that the verified property is the correct one
- Better product line approach: given the verification tool is generic with a collection of property categories and takes a model has input.
- of course, validating data is necessary but not sufficient to ensure the correctness of the system behavior.
- so far, the properties verified are most often simple ones but based on Systereml past experience, it is expected to scale well to more complex properties upon a lot of data provided that associated data are easy enough to extract
- a non trivial task is to identify the property to verify which is not always explicitly written down in the available documentation !
- data extraction effort remains
- (not discussed): effort to get a formal tool certified by a certification authority not familiar with those techniques
- (not discussed): limitations of the proof-based approach vs model-checking based approach (see ProB)
The case study is fully described in the paper .
The Generic Payload Management Unit (GPMU) is the part of the satellite (hardware and software) in charge of hosting the payload software which will provide the set of functions enabling the satellite to fulfill its mission (by contrast with the platform part, which provides basic services like energy sources and positioning system).
In this context the set of considered data are constants that contribute to the configuration of the system. They may be
- physical constants,
- parametric constants which are used to define a command law,
- mission specific constants (which may be uploaded), parametric constants specific to the design choices,
- validation and test data,
- constant produced while defining the configuration data (authors, creation date, version, integrity,...)
Properties link different types of data. They exist independently from the system being active or not and define invariants over the system. Validating data is the act of verifying that the configuration data verify the properties (most often, safety ones) identified. They may be categorised as follow:
- properties relative to the domain of scalar constants. e.g. scalar parameter is defined within its bounds
- equality constraints. e.g. the size of a structure is equal to the value of another parameter,
- parameter typing. e.g. all data loaded in a structure respect the structure type,
- coherence between data. e.g. check that some memory spaces are disjoints for a given partition
The global process is summarised as shown in the figure. It is composed of two main process (and related tools):
- the data extraction for harvesting configuration data from binary objects,
- the core of the data proving which was improved and used over the properties and associ-ated configuration data.
In addition, a formal development platform is also available for checking that the properties are well typed and well defined (i.e. meaningful)
See ProB success story: Productivity Improvement of Data Consistency in Transportation Models
Specific DEPLOY Contributions
Usage of RODIN
- Tool Improvements:
- avoid the need of recompilation of the data extraction upon data type change
- keep track of natural language expression of properties into the formal model to allow validation by domain experts
- user interface for allowing inspection of the data set that falsifies a property, to ease the spotting of the configuration data responsible for the property falsification.
- better RODIN integration
- Removing the problem of identifying properties afterward: having the tools and methods for deploying easy data validation would probably be a good incentive for including property management since the beginning of the system development cycle.
- Provide more complete coverage of the space domain and possibly extend to other domains
- ↑ Mathieu Clabaut, Christophe Metayer, and Éric Morand, Formal Data Validation - Formal Techniques Applied to Verification of Data Properties, Embedded Real Time Software and Systems 2010, Toulouse.