Verification of Timing Properties for Software Behaviors on AUTOSAR Architecture using Process Algebra

Nowadays, the complexity of automotive systems is increasing due to various and diverse functional requirements from the users. The growth of complexity can cause serious problems to the safety of automotive electronic systems because their functions are mainly implemented by software. The development in compliance with international standards for safety, such as ISO 26262, and the use of open and standardized software platform, such as AUTOSAR, are demanded to improve the safety of automotive systems. ISO 26262 recommends use of formal methods for high-level safety-integrity systems. This paper proposes applying formal methods to AUTOSAR software models. In particular, we provide formal specification and verification of software behaviors from AUTOSAR System Timing View, to detect errors that are often happened when software components are integrated. In this paper, we propose a formal verification method for timing analysis of AUTOSAR software models from the viewpoint of System Timing View of AUTOSAR timing extension. For the timing analysis, we use ACSR(Algebra of Communicating and Shared Resources), a process algebra, which can effectively specify important characteristics of real-time systems, such as timing, mutually and exclusively time-consuming use of resources, execution based on resource availability. Models in ACSR can be automatically verified by VERSA, a formal verification tool for ACSR. Furthermore, we conduct a case study on car cruise control system to show feasibility of our approach.