Service-oriented decomposition and verification of hybrid system models using feature models and contracts

被引:4
作者
Liebrenz, Timm [1 ]
Herber, Paula [1 ]
Glesner, Sabine [2 ]
机构
[1] Univ Munster, Embedded Syst Grp, Schlosspl 2, D-48149 Munster, Germany
[2] Tech Univ Berlin, Software & Embedded Syst Engn Grp, Str 17 Juni 135, D-10623 Berlin, Germany
关键词
Hybrid systems; Compositional verification; Theorem proving; Model-driven development; VARIABILITY;
D O I
10.1016/j.scico.2021.102694
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
The design of fault-free hybrid control systems, which combine discrete and continuous behavior, is a challenging task. Their hybrid behavior and further factors make their design and verification challenging: These systems can consist of multiple interacting services, and commonly used design languages, like MATLAB/Simulink do not directly allow for the verification of hybrid behavior. Furthermore, services can be reused in new system designs and sometimes require changes in their structure to fit to the new context. By providing hybrid contracts, which formally define the interface behavior of hybrid system services in differential dynamic logic (dL), and providing a decomposition technique, we enable compositional verification of Simulink models with interacting services. This enables us to use the interactive theorem prover KeYmaera X to prove the correctness of hybrid control systems modeled in Simulink. With the inclusion of feature modeling in the design process and the creation of hybrid contracts, we are able to capture a wider range of behavior, while still enabling the use of formal interface description in the verification. We demonstrate the applicability of our approach with a temperature control system and an automotive industrial case study. (C) 2021 Elsevier B.V. All rights reserved.
引用
收藏
页数:25
相关论文
共 42 条
[1]   Semi-automatic Identification and Representation of Subsystem Variability in Simulink Models [J].
Alalfi, Manar H. ;
Rapos, Eric J. ;
Stevenson, Andrew ;
Stephan, Matthew ;
Dean, Thomas R. ;
Cordy, James R. .
2014 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE MAINTENANCE AND EVOLUTION (ICSME), 2014, :486-490
[2]  
Alur Rajeev, 1992, HYBRID SYSTEMS, P209, DOI [10.1007/3-540-57318, DOI 10.1007/3-540-57318, DOI 10.1007/3-540-57318-630, DOI 10.1007/3-540-57318-6]
[3]  
[Anonymous], MATLAB SIM
[4]  
Araiza-Illan D, 2014, 2014 UKACC INTERNATIONAL CONFERENCE ON CONTROL (CONTROL), P244, DOI 10.1109/CONTROL.2014.6915147
[5]  
Astefanoaei Lacramioara, 2016, Theory and Practice of Formal Methods. Essays Dedicated to Frank de Boer on the Occasion of His 60th Birthday. LNCS 9660, P88, DOI 10.1007/978-3-319-30734-3_8
[6]  
Barnett M, 2006, LECT NOTES COMPUT SC, V4111, P364
[7]   Assume-guarantee verification of nonlinear hybrid systems with ARIADNE [J].
Benvenuti, Luca ;
Bresolin, Davide ;
Collins, Pieter ;
Ferrari, Alberto ;
Geretti, Luca ;
Villa, Tiziano .
INTERNATIONAL JOURNAL OF ROBUST AND NONLINEAR CONTROL, 2014, 24 (04) :699-724
[8]  
Boström P, 2011, LECT NOTES COMPUT SC, V6991, P291, DOI 10.1007/978-3-642-24559-6_21
[9]  
Chen Mingshuai., 2017, Provably Correct Systems, P39
[10]   Computational techniques for hybrid system verification [J].
Chutinan, A ;
Krogh, BH .
IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2003, 48 (01) :64-75