CATSY

The CATSY (Catalogue of System and Software Properties) project aims to improve the early verification and validation (V&V) activities. By providing new methods to formalise requirements, both validation and verification can be performed earlier and more accurately.

The project was started in 2015 and concluded in 2016, carried out by Space Systems Finland (prime contractor), Fondazione Bruno Kessler (research subcontractor) and RWTH Aachen University (research subcontractor).

Project Goals

In order to shorten the system development lifecycle, it is desirable to push V&V activities to the early design phases. This requires an integrated approach where such techniques are not only applied to the final implementation of the system but also to design artefacts that have been produced as intermediate representations of the system. This is the point where model-based system and software engineering approaches become important. They are based on models that describe the possible system behaviour in a mathematically precise and unambiguous manner. To allow for the envisaged benefits of early V&V, they need to be combined with formal methods to enable unambiguous specifications and their formal verification.

Once properties have been verified for a system model produced during a specific phase of the system development lifecycle, it must be ensured that they are preserved during the subsequent development steps. As the latter usually represent some form of refinement activities which add more and more details to an initially abstract system design, the verification problem boils down to establishing that properties are preserved under refinement. In particular, refinement often means that (a part of) the system is split into several sub-systems, each with a dedicated functionality. In this case, compositional reasoning techniques are required that allow to break down the properties of the overall system to properties of the sub-systems such that the successful verification of the sub-properties guarantees the intended behaviour of the overall system.

Clearly, the formal reasoning techniques depend on the kinds of properties to be verified. Usually one distinguishes between correctness, safety, timing, dependability, performance, and security aspects of the system under development. However, these classes are not disjoint such that concrete properties can be categorised in several ways. In addition, within each of the above categories one distinguishes between different property types, such as liveness, safety, and fairness and small variations thereof. This poses another challenge with regard to the integration of formal methods into the system development life cycle, namely, to provide the designers with a classification scheme (or taxonomy) that is oriented towards their needs.

In summary, the project’s objectives can be characterised as follows:

1. Development of approaches to systematically derive (formal) properties from (informal) requirements specifications. This includes the abstraction of classes of similar properties to patterns and the identification of driving properties at the respective phase of the system development.
2. Elaboration of taxonomy of system and software properties that takes both the designer and the formal point of view into account. The intended taxonomy shall encompass properties that can be found at different levels of abstraction of the development process, and all the classes of requirements identified for each level.
3. Identification of modelling languages and supporting tools. Such languages are required for representing both the system under development and its desired properties. To support formal reasoning, both have to be equipped with an unambiguous formal semantics, allowing tool support for carrying out the modelling, specification, and verification activities. As such tool support might not be available for all possible combinations of classes of system models and verification properties; one possible outcome is the identification of technological gaps that need to be closed.
4. Application of the developed methods to practical case studies, to assess the coverage of industrial requirements and the scalability of the approach.
5. Evaluation of the overall approach in term of its adequacy and the implications of its introduction into the existing system development lifecycle. In particular, this evaluation shall produce guidelines for system modelling and requirements specification to enhance the efficiency of the verification activities.