论文标题
用于建模和验证异质系统的多面合同
Multi-Facets Contract for Modeling and Verifying Heterogeneous Systems
论文作者
论文摘要
核电站，铁路，汽车或航空行业等大型行业中存在的关键和网络物理系统（CPS）是复杂的异质系统。它们之所以复杂，是因为它们是开放的，无周边的，通常是通过组装各种异质和相互作用的组件来建造的，这些组件经常由于要求而经常重新配置。因此，对此类系统的建模和分析是软件工程的挑战。我们引入了一种新方法来建模和验证异质系统。该方法包括：为单个组件配备广义合同，根据给定的方面订购这些合同，构成这些组件并验证所得系统相对于方面。我们通过案例研究说明了该方法的使用。可以扩展所提出的方法以覆盖更多的方面，并通过积极的建模和财产验证来加强援助工具。
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.
