| Popis: |
The verifiable design process (VDP) is a systems engineering methodology that integrates formal methods and model based systems engineering to achieve a correct-by-construction system. Formal methods are used in the design process to verify correct behavior of system as specified in the requirements. In order to aid development and analysis, the verifiable design process is organized in abstraction layers. The layers are represented using models that include requirements in natural language form, requirements in ontological form, specifications in logic form together with a proof process and interconnected models and their simulations. The models are intelligently coupled with each other to enable the formal verification and model-based validation of a system. In this work, we will show how to formalize the verifiable design process using category theory. We first show how to represent the different representations (models) of VDP as a category. Suitable categorical structures are employed to analyze them. Furthermore, we define each abstraction layer as a category (category of categories) with the models forming the objects and the relations among them forming the morphisms (functors). We then use pushout structure to represent the objects and their relations to provide analysis of the design process. The functors defined will formalize the relations between the different forms of representations. |
