CATSY Approach
Overall, the CATSY approach aims to assist in the formal specification of informally specified requirements. In the CATSY approach, requirements and requirement-like constraints are categorised in a routine manner in order to encourage recognition of semantic similarity, and use of predefined syntactic patterns in formal models is highly recommended in order to support recognition of syntactic similarity.
Requirements Taxonomy
In this approach, requirements are categorised by taxonomy of requirements. The concerned taxonomy is based on the properties found in the various requirement classes as collected from various ECSS standards. For each class in the taxonomy, a corresponding formalisation is given if possible. This forms the basis of the approach, as the formalisation is used for the verification activities.
Properties
For each individual property in the taxonomy, a distinction is made whether it is formalised by means of modelling (as a structure in the model), as a formal property, or neither. The model describes the architecture of the system, for example redundancy aspects, which is used as a basis to formalise the model’s properties against. These (formal) properties are formulas or expressions in a formal language that describe a certain aspect of the system/model, such as reaction delays, invariants or data monitoring.
CATSY formalisation overview
CSSP
The primary method of formalisation is provided by the CSSP (Catalogue of System and Software Properties), which consists of a set of pre-defined design attributes which are based on the requirements taxonomy. A specific subset of the classes in this taxonomy is mapped to these attributes. The following table lists a fragment of these attributes. These attributes are attached to elements of the design model, such as system components or communication ports. Formal properties are then automatically derived, such that a formal background is not required in order to make use of the CSSP.
| Parameterised formal property | Description |
| PersistentProperty(p) | specifies that the value of data port p changes only on the Change(p) event |
| ModeInhibitedProperty(m) | specifies that the events in ModeInhibited(m) cannot occur in mode m |
| ModeInvariantProperty(m) | specifies a generic invariant for mode m |
| MonitorProperty(p) | specifies that the event MonitorResponse(p) is fired if the value of p falls outside the specified MonitorRange(p) |
| CompleteAlarmProperty(p) | specifies that if failure configuration FailureCondition(p) is entered, the alarm event p follows within AlarmDelay(p) delay |
| CorrectAlarmProperty(p) | specifies that if the alarm event p occurs, it was preceded by entering the failure configuration FailureCondition(p) within AlarmDelay(p) delay |
| RecoveryProperty(p) | specifies that upon event p, eventually the failure configuration FailureCondition(p) is recovered within RecoveryDelay(p) delay |
| CompleteTimeoutProperty(p) | specifies that if p does not occur within Timeout(p), the alarm TimeoutReset(p) must occur |
Patterns
Pattern properties can also be used for formalisation, which are constructed from well-known property patterns. This is a well-known approach in assisting formalisation of requirements, which allows a user to fill placeholders (propositions) in a predefined pattern, which maps to a formal property. To use this some formal background is advisable, in case non-trivial propositions are required.
Direct Specification
Finally, formalisation is possible by means of directly specifying the formal property. This requires expert knowledge of the formalisms use, but is the most powerful.
Requirement Refinement
Requirements are often organised hierarchically: they are specified at every level of the system design, from the overall system to each hardware and software component. The requirement refinement process follows a top-down flow in parallel to the definition of the system architecture. While the system is decomposed into subsystems, the system requirements are decomposed and allocated to the defined subsystems. In turn, every component can be further decomposed into subcomponents and its requirements are therefore decomposed and allocated to the subcomponents. At each level of the decomposition, the whole set of derived requirements must be validated against the higher-level parent requirements.
CATSY uses a contract-based approach to the refinement of properties, and thus their corresponding requirements. The approach details how properties, first specified at system level, are then refined along the architectural decomposition at subsystem level until specifying the properties of software components.
Once the boundaries of the system have been identified and the system requirements have been specified, the requirements are formalised into formal properties over the interface of the system component. In this setting, properties are structured into assumptions and guarantees, and refinement means that while decomposing a component into subcomponent, assumptions on the environment cannot be stronger and guarantees of the implementation cannot be weaker of the upper level. Contract-based refinement is used to verify if the properties of an abstraction level correctly refine the properties of the upper level.
The CATSY approach assumes five project abstraction levels: Mission, Overall-system/System-of-Systems, System, Sub-system, and Equipment. The requirement classes and properties of the aforementioned taxonomy were related to particular project abstraction levels.
CATSY Framework
The CATSY approach is implemented in the project by formalising the requirements using the SLIM language, which has been derived from AADL and is the input formalism used by the COMPASS toolset.
The CATSY project implements the CATSY approach in such a way that all formal models are SLIM input models, and all automated analysis is by means of the COMPASS toolset. The SLIM language (the input language of COMPASS) has been extended to support specifying properties and contracts in an AADL-compliant way, using an AADL property set. We defined the CSSP property set, which is a catalogue of AADL properties with associated a predefined formalisation in temporal logic, to ease the formalisation of design properties that are typically found during the development lifecycle.
Framework Extensions
Three main changes to the SLIM language have been designed during the course of the project: the specification of abstract component; Property associations as defined in the AADL language; and a separation between the configuration of the system described by modes, and the behaviour of one described by states. The last change allows the strict separation of the configuration and behaviour. The backend tools of the toolset have been extended to support the specification and verification of the new types of properties and contracts.
Case Studies
Out of six case studies consisting of software-based space applications, the Solid State Mass Memory (SSMM) sub-system of the BepiColombo mission was chosen to evaluate the CATSY project. The selection was based on to reality-relatedness, availability of information, presence of project abstraction levels, presence of requirement classes and presence of logical expressivity categories.
Selected official requirements of SSMM were modelled in the SLIM language and analysed with the COMPASS toolset. The SSMM information in the present CATSY summary is public due to earlier appearance in the paper “BepiColombo Solid State Mass Memory Employing SpaceWire” by Michele De Meo, Giovanni Saldi, Guido Rosani, Wahida Gasti, Jeff Noyes, James Windsor, Joachim Poeckentrup and Reinhard Eilenberger on pages 134–139 in the Proceedings of SpaceWire-2013.
SSMM is located on-board the BepiColombo Mercury Planetary Orbiter and provides concurrently data storage facilities to payload instruments, the on-board computer (OBC), and telemetry format generator. SSMM consists of hardware, including FPGAs, memory modules, serial lines, and SpaceWire interfaces; and software, consisting of boot software and application software. SSMM is responsible for storing data and providing this data to the downlink functionality during times at which a ground-link has been established. The data can be satellite and/or equipment monitoring data as well as scientific data produced by the payload instruments.
In coarse preliminary analysis, 1852 official requirements were considered suitable for modelling. Among these, we selected and modelled 56 requirements due to the time limit of the evaluation, the iterative adaptation of modelling principles, the development of some COMPASS features in parallel to the evaluation, and due to an intention to avoid unnecessary semantic compromises in modelling. Some of these were even partially modelled, since a complete modelling would have required the interpretation of various superficial expressions, some of which may consider responsibilities of BepiColombo sub-systems other than SSMM.
The modelled requirements concerned communication relationships, Failure Detection, Isolation and Recovery (FDIR), booting and rebooting, and the File Transfer Session part of the SSMM specification of the ECSS-E-ST-70-41C Service 13, “Large Packet Transfer”.
Three SLIM input models and four analysis archives were released in such a way that the released SLIM input models together demonstrate gradual modelling of several requirement levels, whereas the released analysis archives demonstrate how analysis of SLIM contracts can be used for validation of requirement relationships on several requirement levels and across requirement levels, with freedom to use the Command Line Interface of COMPASS or the Graphical User Interface of COMPASS. Three requirement levels were involved in the set of modelled requirements. Refinement of requirements was concretely investigated with respect to two of those three levels. Logical feasibility of the joint effect of requirements was systematically investigated. A small amount of failure probability analysis was included.
All modelled requirements were categorised, and categorisation of the used ways of modelling was provided together with precise identification of associated locations in released SLIM input models. The categorisation was with respect to a set of 93 property types that can be considered suitable for formal modelling. The modelled requirements fall in 16 of these property types.
The case studies also used the CSSP property library, although in a limited way. The released final SLIM input model uses 3 CSSP properties in 6 SLIM contracts. The utilisation of the library was low mainly because the CSSP is meant to express very basic properties while most contracts of the case studies are quite complex. A separate investigation of feasibility of the library was performed independently from the case studies using test examples.
Evaluation of the CATSY Approach
Potential Benefits
The CATSY approach is for verification of requirements, requirement-like constraints and associated relationships such as traceability, in such a way that automated analysis is applied to results of formal modelling that systematically transforms semantic similarity to syntactic similarity. In the CATSY approach, requirements and requirement-like constraints are categorised in a routine manner in order to encourage recognition of semantic similarity, and use of predefined syntactic patterns in formal models is highly recommended in order to support recognition of syntactic similarity.
The CATSY approach is suitable for some of the verification and analysis activities that are required by specific requirements in ECSS standards. However, the CATSY approach is not inherently specific to any industrial domain and can be integrated with any systems engineering process where requirements are supposed to have an important role in expressing the intended behaviour of systems. Identification of suitable project abstraction levels and property types is the minimum effort that is needed for taking the CATSY approach into use in a new application domain. Any further industrialisation activity is likely either application-independent or related to tool support for specific project abstraction levels and property types.
The CATSY team has found out that there is certain motivation and readiness to take the CATSY approach into use for analysis of requirements for electrical and/or electronic systems in road vehicles, trains, railway signalling, nuclear power plants and aviation.
Main Limitations
The main limitations of the CATSY approach concern scalability of modelling and analysis in the number of requirements. Scalability of modelling is to a large extent a matter of how much time is needed for interpretation of requirements and for ensuring that requirements are correctly modelled. Scalability of analysis is related to computational complexity, with the provision that time and resources needed in a single analysis case are not dictated by complexity theory. The case studies in the CATSY project faced the problem of scalability of modelling but did not significantly face the problem of scalability of analysis.
Main Recommendations
Time spent in modelling can be tried to be reduced by means of:
- training and related creation of modelling and toolset usage conventions,
- allocation of modelling activities to requirement authors,
- model maintenance (where a model evolves only as much as needed for taking the requirements evolution into account), and
- reasonably selective modelling (for example focus on requirements that a critical to a mission).
Time spent in analysis can be tried to be reduced by toolset optimisation. Separate research for execution times, memory consumption and disk consumption in use of COMPASS for models of large sets of requirements is highly motivated. Construction of such models is a challenge itself. One possibility is to construct models that are only “inspired by requirements”. Even then there should be some reasonable easily observable correspondence between requirements and models. It should also be considered how to proceed in cases where COMPASS is unable to analyse a given model within reasonable time. One possibility is to split the model with respect to modelled requirements.