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

Embedded systems span a wide range from a small platform of sensors and actuators to distributed systems combining several interacting nodes. Designing such systems includes hardware parts and software parts. The software part acquires in importance since it handles the resources and services to interact with the hardware part. The paper introduces a novel deployment-decision making based on PRISM probabilistic model checker that takes software components and the physical platform to produce a set of deployment candidates. Starting from System Modeling Language (SysML), the process includes mechanisms to extract hardware and software features and carry out a set of deployment candidates. Each candidate should satisfy the reliability property written in Probabilistic Computation Tree Logic. Formally, we capture the underlying semantics of software blocks behaviour expressed as an activity diagram and their generated PRISM code to prove the approach soundness. Illustration relies on the automotive control system to show the applicability of the proposed approach.