Improved Capacity to Model and Prove Complex Systems in the Space Sector
| Success Story|
|Keywords||space, complex system, modelling techniques|
|Source||Space System Finland|
The benefits of adopting a formal methods are not immediate and require a number of steps to be undertaken:
- Become familiar with the method and supporting tools
- Identify the kind of requirements that can be modeled and the benefits of modeling
- Develop best practices to model systems in a specific domain in order to be efficient in producing models
- Assess scalability of language and tool support
Those steps were quite systematically undertaken in the Space Sector and are detailed in this evidence.
of Interest to Project and QA Managers
- TOOL-PQAM-1 What percentage of proof can be automated on average when a formalism is used efficiently?
of Interest to Analysts and Developers
- EM-EA-2 Is a formalism adapted to model important issues in a given application domain?
- TOOL-EA-1 Are the tools available for a formalism reliable?
- TOOL-EA-2 Are tools functionality automating all tedious tasks?
- Capacity to model complex space systems and prove them completely
- Weakness in the type system (record, enumerations, real/rational numbers, abstract data types), preventing to fully capture all the details of the pilots (this is a show stopper).
- Time spent in manual proofs, often requiring repeating very similar steps over and over. The prover should be improved to reach a higher rate of automated proofs, e.g. by supporting the definition of prover tactics.
- Lack of modularity, essential to manage large models.
- Team work is missing and models breaks easily when several people work on the same model.
- Model readability (decomposition, some cryptic syntax).
The initial pilot problem was the BepiColombo probe. Only part of the requirements (about 18% of the real system: 86/408 requirements) were covered. The focus was on the telemetry and tele-command part as it is a key part of all the space systems.
A number of versions of the BepiColumbo were developed iteratively (5 major versions), starting from scratch a number of time to experiments with various way to model that system as part of the learning process which was still on-going but also to try different structuring and refinement strategies in order to discover the respective advantages/disadvantages of each strategy to eventually select the one providing the better solution.
The resulting models were quite complex but most of the efforts were spent not in writing them but rather in proving them. The last version of the model has 8 refinement steps and more than 1000 proof obligations all discharged. Only 68% were automatically discharged. However the manual proofs were composed of a number of very similar manual steps and required tedious repetition that should be readily automated in future.
A second model was developed for an AOCS (Attitude and Orbit Control System) system. The model was even bigger: it has 13 refinement steps and 1858 generated proof obligations. All these proof obligations have been discharged, about 70% automatically in this case.
A complete model has been elaborated from scratch in another round of an Attitude and Orbit Control System (AOCS). AOCS is a complex mode-rich system, which has an intricate mode-transition scheme. We show that refinement in Event B provides the engineers with a scalable formal technique that enables both development of mode-rich systems and proof-based verification of their mode consistency .
- Åbo Akademi contributed some version of the same problems.
- Åbo Akademi also analysed the models in order to develop some complexity metrics .
- ↑ Iliasov, Alexei and Troubitsyna, Elena and Laibinis, Linas and Romanovsky, Alexander and Varpaaniemi, Kimmo and Ilic, Dubravka and Latvala, Timo (2010) Developing Mode-Rich Satellite Software by Refinement in Event B. In: 15th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 2010), September 20-21, 2010, Antwerp, Belgium.
- ↑ Marta Plaska, Kaisa Sere, Towards Event-B specification metrics, in Proceedings of DEPLOY Technical Workshop 2009, Technical Report of the School of Computing Science, Newcastle University (M. Mazzara et al. Eds.), 2010.
<ref> tag with name "D20" defined in
<references> is not used in prior text.