Actor-based Timing Analysis in Automotive Systems

Automotive systems are time-critical; satisfying their timed properties is crucial. One group of popular timed properties for automotive industries is TADL2 timing constraints. Technically, these properties indicate that proper actions must be taken by the system at appropriate times with respect to the environment. Moreover, modern automotive systems consist of interconnected networks of distributed Electronic Control Units (ECUs). In this thesis, I have developed an actor-based framework to verify TADL2 timing constraints in distributed ECUs networks. To address the modeling of distributed networks of ECUs, I have developed the Colored Timed Rebeca (CTRebeca), an extension of Timed Rebeca, with an operational semantic and used TCTL to specify TADL2 timing constraints. To tackle the verification problem, I have implemented a model checking algorithm to check TCTL formulas against the CTRebeca models.