Catalogue of System and Software Properties

The use of formal methods has been recognized in different domains as a potential means for early validation and verification. However, correctly specifying formal properties is difficult due to the ambiguity of the typical textual requirements and the complexity of the formal languages. To address this, we define the Catalogue of System and Software Properties. Starting from a taxonomy of requirements extracted from space standards, we derive a list of design attributes divided per requirement type. We map these design attributes to AADL system architectures and properties, for which we define formal semantics and properties. We exemplify the approach using AADL models taken from the space domain.