//This file was generated from UPPAAL2k. /* 1996-11-20, 1997-02-20--27, and 1997-07-31 @ Uppsala University Paul Pettersson and Wang Yi, DoCS, Uppsala University and Magnus Lindahl, Mecel AB. OVERVIEW This document is the specification file engine.q. It is written in UPPAAL2k's q-format and can be used in the tool to check properties of the gearbox controller. The system is modelled in the file engine.{xta|ugi}. E1 to E11 are requirements on the environment of the gearbox controller, that should be respected by the formal model of the environment. R1 to R9 are requirements on the gearbox controller design given by Mecel AB in natural language. P1 to P17 formalize R1 to R9, that should be satisfied by the formal model of the gearbox controller. INFORMAL REQUIREMENTS ON THE ENVIRONMENT OF GEARBOX CONTROLLER E1 to E11 are requirements that the environment of the gearbox controller design should satisfy to guarantee the behavior of the whole system works properly. That is, if any of the assumptions E1 to E11 are not satisfied by the environment then P1 to P17 are *not* guaranteed to hold: E1. Initially the clutch is closed. E2. To open the clutch, it takes at least 100 ms and at most 150 ms. E3. To close the clutch, it takes at least 100 ms and at most 150 ms. E4. Initially the gearbox is neutral. E5. To release the gear, it takes at least 100 ms and at most 200 ms. E6. To set a gear, it takes at least 100 ms and at most 300 ms. E7. The engine is always in a predefined state called "Initial" when no gear is set. E8. To find zero torque in the engine, it takes at least 150 ms and at most 400 ms. But at 400 ms, the engine may enter an error state or find zero torque. E9. To find synchronous speed, it takes at least 50 ms and at most 200 ms. But at 200 ms the engine may enter an error state or find synchronous speed. E10. The engine may regulate on synchronous speed in at most 500 ms. E11. When in an error state, the engine will regulate on synchronous speed in at least 50 ms and at most 500 ms. INFORMAL REQUIREMENTS ON THE GEARBOX CONTROLLER DESIGN The Gearbox controller should satisfy the following informal requirements. The properties given in parentheses are the formal description of the listed requirement. R1. A gear change should be performed within 1 second (P6 - P8, P3). R2. When an error arises, the system will reach a predefined error state marking the error (P9 - P11). R3. The system should be able to use all gears (P2 - P3). R4. There will be no deadlocked state in the system (P17). R5. When the system indicates gear neutral, the engine should be in initial state (P12). R6. When the system indicates a gear, the engine should be in a state performing torque regulation (P13). R7. The gearbox controller will never indicate open or closed clutch when the clutch is closed or open respectively (P14). R8. The gearbox controller will never indicate gear set or gear neutral when the gear is not set or not idle, respectively (P15). R9. When the engine is regulating on torque, the clutch is closed (P16). FORMALIZING THE REQUIREMENTS The requirements above have been formalised using variables and locations of automata. The system variables listed below are variables used by the components of the system; the auxiliary variables are decorations to the system used to formalize the requirements only. In the system description, the auxiliary variables appear only in assignments (not in guards). This ensures that the system behavior is not changed when the auxiliary variables are introduced (or removed). The variables ErrStat and UseCase are used to trace errors. ErrStat is set when unrecoverable errors occur; UseCase is set when recoverable errors occur, that will be recovered by the gearbox controller. The systems component locations that appear in the formulae below can be found in the system description file engine.{xta|ug}. System Variables: o GCTimer - gearbox controller timer, o ETimer - engine timer, o GBTimer - gearbox timer, o CTimer - clutch timer, o FromGear - selected gear before gear change (0=N, 1=1, ..., 6=R), o ToGear - selected gear after gear change (0=N, 1=1, ..., 6=R). Auxiliary Variables: o SysTimer - system timer, reset at each request for new gear (in the gearbox controller), o ErrStat - 0 = no errors, 1 = close clutch error, 2 = open clutch error, 3 = set gear failure, 4 = error releasing gear. o UseCase - 0 = ideal scenario, no problems occurred, 1 = engine was not able to deliver zero torque, 2 = engine was not able to find synchronous speed. */ //NO_QUERY /* P1. It is possible to change gear. */ E<> GearControl.GearChanged /* P2. It is possible to switch to gear nr 5... */ E<> ( Interface.Gear5 ) /* ...and to reverse gear (i.e. R). */ E<> ( Interface.GearR ) /* P3. It is possible to switch gear in 1000 ms (not very interesting). */ E<> ( GearControl.GearChanged and ( SysTimer<=1000 ) ) /* P4. When the gearbox is in position N, the gear is not in position 1-5 or R. */ A[] not ( GearBox.Neutral and \ ( Interface.Gear1 or Interface.Gear2 or \ Interface.Gear3 or Interface.Gear4 or \ Interface.Gear5 or Interface.GearR ) ) /* P5. The gear is never N, when the gearbox is idle... */ A[] not ( GearBox.Idle and Interface.GearN ) /* ...in fact, gearbox is neutral when gear is neutral. */ A[] ( Interface.GearN imply GearBox.Neutral ) /* P6. In the case of no errors (in gear and clutch) and ideal a) a gear switch is guaranteed in 900 ms (including 900 ms), */ A[] ( ( ErrStat==0 and UseCase==0 and SysTimer>=900 ) imply \ ( GearControl.GearChanged or GearControl.Gear ) ) /* a') a gear switch is not guaranteed in strictly less than 900 ms, */ E<> ( ErrStat==0 and UseCase==0 and \ SysTimer>899 and SysTimer<900 and \ not ( GearControl.GearChanged or GearControl.Gear ) ) /* b) it is impossible to switch gear in less than 150 ms, */ A[] ( ( ErrStat==0 and UseCase==0 and ( SysTimer<150 ) ) imply \ not ( GearControl.GearChanged ) ) /* b') it is possible to switch gear at 150 ms, */ E<> ( ErrStat==0 and UseCase==0 and GearControl.GearChanged and \ ( SysTimer==150 ) ) /* c) it is impossible to switch gear in less than 400 ms if the switch is not from/to gear N. */ A[] ( ( ErrStat==0 and UseCase==0 and FromGear>0 and \ ToGear>0 and ( SysTimer<400 ) ) imply \ not ( GearControl.GearChanged ) ) /* c') it is possible to switch gear at 400 ms if the switch is not from/to gear N. */ E<> ( ErrStat==0 and UseCase==0 and FromGear>0 and ToGear>0 and \ GearControl.GearChanged and ( SysTimer==400 ) ) /* P7. When no errors (in gear and clutch) occur, but engine fails to deliver zero torque: a) a gear switch is guaranteed after 1055 ms (not including 1055), */ A[] ( ( ErrStat==0 and UseCase==1 and SysTimer>1055 ) imply \ ( GearControl.GearChanged or GearControl.Gear ) ) /* a') it is impossible to switch gear in 1055 ms, */ E<> ( ErrStat==0 and UseCase==1 and SysTimer==1055 and \ not ( GearControl.GearChanged or GearControl.Gear ) ) /* b) it is impossible to switch gear in less than 550 ms, */ A[] ( ( ErrStat==0 and UseCase==1 and SysTimer<550 ) imply \ not ( GearControl.GearChanged or GearControl.Gear ) ) /* b') it is possible to switch gear at 550 ms, */ E<> ( ErrStat==0 and UseCase==1 and GearControl.GearChanged and \ ( SysTimer==550 ) ) /* c) it is impossible to switch gear in less than 700 ms if the switch is not from/to gear N */ A[] ( ( ErrStat==0 and UseCase==1 and FromGear>0 and \ ToGear>0 and SysTimer<700 ) imply \ not ( GearControl.GearChanged and GearControl.Gear ) ) /* c') it is possible to switch gear at 700 ms if the switch is not from/to gear N. */ E<> ( ErrStat==0 and UseCase==1 and FromGear>0 and ToGear>0 and \ GearControl.GearChanged and \ ( SysTimer==700 ) ) /* P8. When no errors occur, but engine fails to find synchronous speed: a) a gear switch is guaranteed in 1205 ms (including 1205), */ A[] ( ( ErrStat==0 and UseCase==2 and SysTimer>=1205 ) imply \ ( GearControl.GearChanged or GearControl.Gear ) ) /* a') a gear switch is not guaranteed at less than 1205 ms, */ E<> ( ErrStat==0 and UseCase==2 and SysTimer>1204 and \ SysTimer<1205 and \ not ( GearControl.GearChanged or GearControl.Gear ) ) /* b) it is impossible to switch gear in less than 450 ms, */ A[] ( ( UseCase==2 and ( SysTimer<450 ) ) imply \ not ( GearControl.GearChanged or GearControl.Gear ) ) /* b') it is possible to switch gear at 450 ms, */ E<> ( UseCase==2 and GearControl.GearChanged and \ ( SysTimer==450 ) ) /* c) it is impossible to switch gear in less than 750 ms if the switch is not from/to gear N. */ A[] ( ( ErrStat==0 and UseCase==2 and FromGear>0 and \ ToGear>0 and SysTimer<750 ) imply \ not ( GearControl.GearChanged and GearControl.Gear ) ) /* c) it is impossible to switch gear in less than 750 ms if the switch is not from/to gear N. */ E<> ( ErrStat==0 and UseCase==2 and FromGear>0 and ToGear>0 and \ GearControl.GearChanged and \ ( SysTimer==750 ) ) /* P9. Clutch Errors. a) If the clutch is not closed properly (i.e. a timeout occurs) the gearbox controller will enter the location CCloseError within 200 ms. */ A[] ( ( Clutch.ErrorClose and ( GearControl.GCTimer>200 ) ) imply \ GearControl.CCloseError ) /* b) When the gearbox controller enters location CCloseError, there is always a problem in the clutch with closing the clutch. */ A[] ( GearControl.CCloseError imply Clutch.ErrorClose ) /* P9. Clutch Errors (cont.) c) If the clutch is not opened properly (i.e. a timeout occurs) the gearbox controller will enter the location COpenError within 200 ms. */ A[] ( ( Clutch.ErrorOpen and ( GearControl.GCTimer>200 ) ) imply \ GearControl.COpenError ) /* d) When the gearbox controller enters location COpenError, there is always a problem in the clutch with opening the clutch. */ A[] ( ( GearControl.COpenError ) imply Clutch.ErrorOpen ) /* P10. Gearbox Errors. a) If the gearbox can not set a requested gear (i.e a timeout occurs) the gearbox controller will enter the location GSetError within 350 ms. */ A[] ( ( GearBox.ErrorIdle and ( GearControl.GCTimer>350 ) ) imply \ GearControl.GSetError ) /* b) When the gearbox controller enters location GSetError, there is always a problem in the gearbox with setting the gear. */ A[] ( ( GearControl.GSetError ) imply GearBox.ErrorIdle ) /* P10. Gearbox Errors (cont). c) If the gearbox can not switch to neutral gear (i.e. a timeout occurs) the gearbox controller will enter the location GNeuError within 250 ms. */ A[] ( ( GearBox.ErrorNeu and ( GearControl.GCTimer>250 ) ) imply \ GearControl.GNeuError ) /* d) When the gearbox controller enters location GNeuError there is always a problem in the gearbox with switching to neutral gear. */ A[] ( ( GearControl.GNeuError ) imply GearBox.ErrorNeu ) /* P11. If no errors occur in the engine, it is guaranteed to find synchronous speed. */ A[] not ( ErrStat==0 and Engine.ErrorSpeed ) /* P12. When the gear is N, the engine is in initial or on its way to initial (i.e. ToGear==0 and engine in zero). */ A[] ( Interface.GearN imply \ ( ( ToGear==0 and Engine.Zero ) or Engine.Initial ) ) /* P13. When the gear controller has gear R set, torque regulation is always indicated in the engine. */ A[] ( ( GearControl.Gear and Interface.GearR ) imply \ Engine.Torque ) /* - " - gear 1 - " - */ A[] ( ( GearControl.Gear and Interface.Gear1 ) imply \ Engine.Torque ) /* - " - gear 2 - " - */ A[] ( ( GearControl.Gear and Interface.Gear2 ) imply \ Engine.Torque ) /* - " - gear 3 - " - */ A[] ( ( GearControl.Gear and Interface.Gear3 ) imply \ Engine.Torque ) /* - " - gear 4 - " - */ A[] ( ( GearControl.Gear and Interface.Gear4 ) imply \ Engine.Torque ) /* - " - gear 5 - " - */ A[] ( ( GearControl.Gear and Interface.Gear5 ) imply \ Engine.Torque ) /* P14. a) If clutch is open, the gearbox controller is in one of the predefined locations. */ A[] ( Clutch.Open imply \ ( GearControl.ClutchOpen or GearControl.ClutchOpen2 or \ GearControl.CheckGearSet2 or GearControl.ReqSetGear2 or \ GearControl.GNeuError or \ GearControl.ClutchClose or \ GearControl.CheckClutchClosed or \ GearControl.CheckClutchClosed2 or \ GearControl.CCloseError or \ GearControl.GSetError or GearControl.CheckGearNeu2 ) ) /* b) If clutch is closed, the gearbox controller is in one of the predefined locations. */ A[] ( Clutch.Closed imply \ ( GearControl.ReqTorqueC or GearControl.GearChanged or \ GearControl.Gear or GearControl.Initiate or \ GearControl.CheckTorque or GearControl.ReqNeuGear or \ GearControl.CheckGearNeu or GearControl.GNeuError or \ GearControl.ReqSyncSpeed or \ GearControl.CheckSyncSpeed or GearControl.ReqSetGear or \ GearControl.CheckGearSet1 or GearControl.GSetError ) ) /* P15. a) If gear is set, the gearbox controller is in one of the predefined locations. */ A[] ( GearBox.Idle imply \ ( GearControl.ClutchClose or \ GearControl.CheckClutchClosed or \ GearControl.CCloseError or \ GearControl.ReqTorqueC or GearControl.GearChanged or \ GearControl.Gear or GearControl.Initiate or \ GearControl.CheckTorque or GearControl.ReqNeuGear or \ GearControl.CheckClutch2 or GearControl.COpenError or \ GearControl.ClutchOpen2 ) ) /* b) If gear is neutral, the gearbox controller is in one of the predefined locations. */ A[] ( GearBox.Neutral imply \ ( GearControl.ReqSetGear or \ GearControl.CheckClutchClosed2 or \ GearControl.CCloseError or GearControl.ReqTorqueC or \ GearControl.GearChanged or GearControl.Gear or \ GearControl.Initiate or GearControl.ReqSyncSpeed or \ GearControl.CheckSyncSpeed or GearControl.ReqSetGear or \ GearControl.CheckClutch or GearControl.COpenError or \ GearControl.ClutchOpen or GearControl.ReqSetGear2 ) ) /* P16. If engine regulates on torque, then the clutch is closed. */ A[] ( Engine.Torque imply Clutch.Closed )