/////////////////////////////////////////////////////////////////////////////// // 1996-11-20, 1997-02-20--27, and 1997-07-31 @ Uppsala University // Paul Pettersson, DoCS and Magnus Lindahl, Mecel AB. /////////////////////////////////////////////////////////////////////////////// // // OVERVIEW // // This specification file (engine.q) comply with UPPAALs q-format. It is the // actual input file used to check properties of the gearbox controller. The // system is modelled in the file engine.atg. To verify the system run: // 'atg2ta engine.atg engine.ta' and 'verifyta -sT engine.ta engine.q'. // // E1 to E11 are requirements on the environment of the gearbox controller, // R1 to R9 are requirements on the gearbox controller design given by // Mecel AB. P1 to P15 are properties satisfied by the gearbox controller. // P1 to P16 prove R1 to R8 (given that E1 to E11 holds). // // // REQUIREMENTS ON THE ENVIRONMENT OF GEARBOX CONTROLLER DESIGN // // E1 to E11 are requirements that the environment of the gearbox controller // design should satisfy to guarantee the behavior of the controller. That is, // if any of the requirements E1 to E11 are not satisfied by the environment // then P1 to P15 are *not* guaranteed to hold: // // E1. Initially the clutch is closed. // // E2. To open the clutch (a) at least 100 ms and (b) at most 150 ms is needed. // // E3. To close the clutch (a) at least 100 ms and (b) at most 150 ms is // needed. // // E4. Initially the gearbox is neutral. // // E5. To release the gear (a) at least 100 ms and (b) at most 200 ms is // needed. // // E6. To set a gear (a) at least 100 ms and (b) at most 300 ms is needed. // // E7. The engine is always in a predefined state called "Initial" // (a) initially, and (b) when no gear is set. // // E8. To find zero torque in the engine (a) at least 150 ms and (b) at // most 400 ms are needed. (c) At 400 ms the engine will enter an error // state or find zero torque. // // E9. To find synchronous speed (a) at least 50 ms and (b) at most 200 ms are // needed. (c) At 200 ms the engine will enter an error state or find // synchronous speed. // // E10. The engine may regulate on synchronous speed at most 500 ms. // // E11. When in error state the engine will regulate on synchronous speed // at least 50 ms ( and at most 500 ms ). // // // REQUIREMENTS ON THE GEARBOX CONTROLLER DESIGN // // The Gearbox Controller should satisfy the following informal // requirements. The number within parentheses refers to the properties // that ensures that the requirement is satisfied: // // R1. A gear change is performed in 1 second (P6 - P8, P3) (*). // // R2. When an specific error arise the system will end in a known error // state that points out the specific error (P9 - P11). // // R3. The system should be able to use all gears (P2-P3). // // R4. There will be no dead-locks or live-locks in the system. (R1). // // R5. When the system indicate gear neutral the engine will indicate // initial state (P12). // // R6. When the system indicate a gear the engine will indicate 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). // // (*) If an ideal gear change scenario is considered (without the occurrence // of errors) the change is guaranteed within 900 ms and will consume // at least 150 ms. If a gear change not involving gear N is considered // the change will consume at least 400 ms. A gear change may take up // to 1205 ms when successful but less ideal scenarios (with occurrence // of errors) are considered. // // // FORMALIZING THE REQUIREMENT // // The requirement 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 formalise the requirements only. In the system 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 when recoverable errors, // which are resolved by the gearbox controller, occur. // // The systems component locations that appears in the formulae below can // be found in the system description file engine.{atg|ta}. // // 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. // // /////////////////////////////////////////////////////////////////////////////// // ---------------------------------------------------------------------------- // P1. It is possible to change gear. // ---------------------------------------------------------------------------- E<> GearControl.GearChanged // ---------------------------------------------------------------------------- // P2. It is possible to switch to gear nr 5 and to reverse (=R) gear. // ---------------------------------------------------------------------------- // a) E<> Interface.Gear5 // b) 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 (expected to be neutral). // ---------------------------------------------------------------------------- // a) A[] not ( GearBox.Idle and Interface.GearN ) // b) A[] ( Interface.GearN imply GearBox.Neutral ) // ---------------------------------------------------------------------------- // P6. If no errors (in gear and clutch) and ideal (engine) scenario: // a) a gear switch is guaranteed in 900 ms (including 900), // a') a gear switch is not guaranteed in less than 900 ms, // b) it is impossible to switch gear in less than 150 ms, // b') it is possible to switch gear at 150 ms, // c) it is impossible to switch gear in less than 400 ms if the switch is // not from/to gear N. // c') it is possible to switch gear at 400 ms if the switch is not from/to // gear N. // ---------------------------------------------------------------------------- // a) A[] ( ( ErrStat==0 and UseCase==0 and SysTimer>=900 ) imply \ ( GearControl.GearChanged or GearControl.Gear ) ) // a') E<> ( ErrStat==0 and UseCase==0 and SysTimer>899 and SysTimer<900 and \ not ( GearControl.GearChanged or GearControl.Gear ) ) // b) A[] ( ( ErrStat==0 and UseCase==0 and ( SysTimer<150 ) ) imply \ not ( GearControl.GearChanged ) ) // (In (b) GearControl.Gear is not implied since the property is then // satisfied by the systems initial state.) // b') E<> ( ErrStat==0 and UseCase==0 and GearControl.GearChanged and \ ( SysTimer==150 ) ) // c) A[] ( ( ErrStat==0 and UseCase==0 and FromGear>0 and ToGear>0 and \ ( SysTimer<400 ) ) imply \ not ( GearControl.GearChanged ) ) // c') E<> ( ErrStat==0 and UseCase==0 and FromGear>0 and ToGear>0 and \ GearControl.GearChanged and ( SysTimer==400 ) ) // ---------------------------------------------------------------------------- // P7. If no errors (in gear and clutch) but engine fails to deliver zero // torque: // a) a gear switch is guaranteed after 1055 ms (not including 1055), // a') it is impossible to switch gear in 1055 ms, // b) it is impossible to switch gear in less than 550 ms, // b') it is possible to switch gear at 550 ms, // c) it is impossible to switch gear in less than 700 ms if the switch is // not from/to gear N. // c') it is possible to switch gear at 700 ms if the switch is not from/to // gear N. // ---------------------------------------------------------------------------- // a) A[] ( ( ErrStat==0 and UseCase==1 and SysTimer>1055 ) imply \ ( GearControl.GearChanged or GearControl.Gear ) ) // a') E<> ( ErrStat==0 and UseCase==1 and SysTimer==1055 and \ not ( GearControl.GearChanged or GearControl.Gear ) ) // b) A[] ( ( ErrStat==0 and UseCase==1 and SysTimer<550 ) imply \ not ( GearControl.GearChanged or GearControl.Gear ) ) // b') E<> ( ErrStat==0 and UseCase==1 and GearControl.GearChanged and \ ( SysTimer==550 ) ) // c) A[] ( ( ErrStat==0 and UseCase==1 and FromGear>0 and ToGear>0 and \ SysTimer<700 ) imply \ not ( GearControl.GearChanged and GearControl.Gear ) ) // c') E<> ( ErrStat==0 and UseCase==1 and FromGear>0 and ToGear>0 and \ GearControl.GearChanged and \ ( SysTimer==700 ) ) // ---------------------------------------------------------------------------- // P8. If no errors but engine fails to find synchronous speed: // a) a gear switch is guaranteed in 1205 ms (including 1205), // a') a gear switch is not guaranteed at less than 1205 ms, // b) it is impossible to switch gear in less than 450 ms, // b') it is possible to switch gear at 450 ms, // c) it is impossible to switch gear in less than 750 ms if the switch is // not from/to gear N. // c') it is possible to switch gear at 750 ms if the switch is not from/to // gear N. // ---------------------------------------------------------------------------- // a) A[] ( ( ErrStat==0 and UseCase==2 and SysTimer>=1205 ) imply \ ( GearControl.GearChanged or GearControl.Gear ) ) // a') E<> ( ErrStat==0 and UseCase==2 and SysTimer>1204 and SysTimer<1205 and \ not ( GearControl.GearChanged or GearControl.Gear ) ) // b) A[] ( ( UseCase==2 and ( SysTimer<450 ) ) imply \ not ( GearControl.GearChanged or GearControl.Gear ) ) // b') E<> ( UseCase==2 and GearControl.GearChanged and \ ( SysTimer==450 ) ) // c) A[] ( ( ErrStat==0 and UseCase==2 and FromGear>0 and ToGear>0 and \ SysTimer<750 ) imply \ not ( GearControl.GearChanged and GearControl.Gear ) ) // c') 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 gear- // box controller will enter the location CCloseError within 200 ms. // b) When the gearbox controller enters location CCloseError, there is // always a problem in the clutch with closing the clutch. // ---------------------------------------------------------------------------- // a) A[] ( ( Clutch.ErrorClose and ( GCTimer>200 ) ) imply \ GearControl.CCloseError ) // b) A[] ( GearControl.CCloseError imply Clutch.ErrorClose ) // ---------------------------------------------------------------------------- // P9. Clutch Errors (cont.) // c) If the clutch is not opened properly (i.e. a timeout occurs) the gear- // box controller will enter the location COpenError within 200 ms. // d) When the gearbox controller enters location COpenError there is always // a problem in the clutch with opening the clutch. // ---------------------------------------------------------------------------- // c) A[] ( ( Clutch.ErrorOpen and ( GCTimer>200 ) ) imply GearControl.COpenError ) // d) 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. // b) When the gearbox controller enters location GSetError there is always // a problem in the gearbox with setting the gear. // ---------------------------------------------------------------------------- // a) A[] ( ( GearBox.ErrorIdle and ( GCTimer>350 ) ) imply GearControl.GSetError ) // b) 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 200 ms. // d) When the gearbox controller enters location GNeuError there is always // a problem in the gearbox with switching to neutral gear. // ---------------------------------------------------------------------------- // c) A[] ( ( GearBox.ErrorNeu and ( GCTimer>200 ) ) imply GearControl.GNeuError ) // d) 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 gear N then 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 have a gear set, torque regulation is always // indicated in the engine. // ---------------------------------------------------------------------------- // a) A[] ( ( GearControl.Gear and Interface.GearR ) imply Engine.Torque ) // b) A[] ( ( GearControl.Gear and Interface.Gear1 ) imply Engine.Torque ) // c) A[] ( ( GearControl.Gear and Interface.Gear2 ) imply Engine.Torque ) // d) A[] ( ( GearControl.Gear and Interface.Gear3 ) imply Engine.Torque ) // e) A[] ( ( GearControl.Gear and Interface.Gear4 ) imply Engine.Torque ) // f) A[] ( ( GearControl.Gear and Interface.Gear5 ) imply Engine.Torque ) // ---------------------------------------------------------------------------- // P14. a) If clutch is open then the gearbox controller is in location... // b) If clutch is closed then the gearbox controller is in location... // ---------------------------------------------------------------------------- // a) 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) 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 then the gearbox controller is in location... // b) If gear is neutral then the gearbox controller is in location... // ---------------------------------------------------------------------------- // a) 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) 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 ) ////////////////////////////////// - end - ////////////////////////////////////