Formal Design and Analysis of a Gear Controller

In this paper, we report on an application of the validation and veri cation tool kit Uppaal in the design and analysis of a prototype gear controller, carried out in a joint project between industry and academia. The gear controller is a component in the control system operating in a modern vehicle, implementing the gear change algorithm. We give a detailed description of the formal model of the gear controller and its surrounding environment, and its correctness formalized in 46 logical formulas according to the informal requirements delivered by our industrial partner of the project. The second contribution of this paper is a solution to the problem we met in this case study, namely how to use a tool like Uppaal, which only provides reachability analysis to verify bounded response time properties e.g. if f1 a request becomes true at a certain time point, then f2 a response must be guaranteed to hold within a given time bound. We present a logic and a method to characterize and model...

• Type: Conference
• Year: 1998
• Where: TACAS
• Authors: Magnus Lindahl, Paul Pettersson, Wang Yi
• Keywords: Algorithms, Gear Controller, Prototype Gear Controller, Reachability Analysis, TACAS 1998