Multi-Facets Contract for Modeling and Verifying Heterogeneous Systems

TL;DR

This paper presents a novel method for modeling and verifying complex heterogeneous systems by using generalized contracts, facet-based ordering, and composition, demonstrated through a case study.

Contribution

It introduces a new approach for modeling and verifying heterogeneous systems using multi-faceted contracts and composition, enhancing analysis capabilities.

Findings

Effective modeling of heterogeneous systems using generalized contracts

Successful verification of system properties through facet-based composition

Potential for extending the method to additional facets and tools

Abstract

Critical and cyber-physical systems (CPS) that exist in large industries, such as nuclear power plants, railway, automotive or aeronautical industries are complex heterogeneous systems. They are complex because they are open, perimeter-less, often built by assembling various heterogeneous and interacting components which are frequently reconfigured due to requirements. Consequently, the modeling and analysis of such systems is a challenge in software engineering. We introduce a new method for modeling and verifying heterogeneous systems. The method consists in: equipping individual components with generalized contract, ordering these contracts according to given facets, composing these components and verifying the resulting system with respect to the facets. We illustrate the use of the method by a case study. The proposed method may be extended to cover more facets, and by strengthening assistance tool through proactive aspects in modelling and property verification.