Reliability-driven Automotive Software Deployment based on a Parametrizable Probabilistic Model Checking

作者：

Highlights：

• Reliability-driven deployment optimization for automotive control system.

• The system is modeled by SysML internal block diagrams and activity diagrams.

• SysML activity diagrams are captured formally in a proposed calculus.

• We translate the model into PRISM language.

• The soundness of the proposed framework is proved.

摘要

•Reliability-driven deployment optimization for automotive control system.•The system is modeled by SysML internal block diagrams and activity diagrams.•SysML activity diagrams are captured formally in a proposed calculus.•We translate the model into PRISM language.•The soundness of the proposed framework is proved.

论文关键词：SysML internal block diagrams,Activity diagrams,Reliability,Model checking,Deployment

论文评审过程：Received 27 May 2020, Revised 1 January 2021, Accepted 3 January 2021, Available online 8 January 2021, Version of Record 7 March 2021.

论文官网地址：https://doi.org/10.1016/j.eswa.2021.114572