SWE623 Project in OCL: Circular Railroad with a Gate

SWE623 Project in OCL: Circular Railroad with a Gate

Prepared by: Donna Voigt (231-82-5551)

11/30/2000

ASSUMPTIONS:

The train is moving on a circular track 5000 meters long

The Gate location is at 0 meters and the track is measured incrementally in the direction the train is travelling

The initial train location is at 101 meters, therefore the train is in the PAST state and 50 <= train speed <=30

The train never stops

There is only one train on the track.

The train is < 100 meters long

1 / Context: / Train
1.1
1.2
1.3
1.4 / Inv:
Inv:
Inv:
Inv: / TrainSpeed >= 30
CurrentLocation >= EXITLOCATION and CurrentLocation < APPROACHLOCATION implies TrainLocation = #FAR
CurrentLocation >=APPROACHLOCATION and CurrentLocation <= TrackLength implies TrainLocation = #NEAR
CurrentLocation >=GATELOCATION and CurrentLocation < EXITLOCATION impliesTrainLocation = #PAST
1.5 / Context: / Train::ComputeLocation()
Inv:
Inv: /

StartTravelTime <= CurrentTime

CurrentLocation <= TrackLength
Pre: / none
Post:
Post:
Post:
Post: / CurrentLocation= CurrentLocation@pre + (ElapsedSeconds * TrainSpeed/3600)
If CurrentLocation = APPROACHLOCATION then to self send SendSignal(#APPROACH) endif
If CurrentLocation = EXITLOCATION then to self send SendSignal(#EXIT) endif
If CurrentLocation = GATELOCATION then SetState(#PAST) endif
1.6 / Context: / Train::SetState(NewState)
Inv: / NewState = #NEAR or NewState = #FAR or NewState = #PAST
Pre: / CurrentLocation =APPROACHLOCATION or
CurrentLocation = GATELOCATION or
CurrentLocation =EXITLOCATION
Post:
Action:
Post:
Action:
Post:
Action: / If NewState = #NEAR then TrainLocation = #NEAR endif
To self send LowerSpeed()
If NewState = #FAR then TrainLocation = #FAR endif
To self send RaiseSpeed()
If NewState = #PAST then TrainLocation = #PAST endif
To self send LowerSpeed()
1.7 / Context: / Train::SendSignal(Signal)
Inv: / Signal = #APPROACH or Signal = #EXIT
Pre: / (CurrentLocation = APPROACHLOCATION and TrainLocation = #FAR) or
(CurrentLocation = EXITLOCATION and TrainLocation = #PAST)
Post:
Action:
Post:
Action: / If Signal = #APPROACH then
To GateController send ProcessEvent(#APPROACH) endif
To self send SetState(#NEAR)
If Signal = #EXIT then
To GateController send ProcessEvent(#EXIT) endif
To self send SetState(#FAR)
1.8 / Context: / Train::LowerSpeed()
Inv: / TrainSpeed >=30 and TrainSpeed <=50
Pre: / TrainLocation = #NEAR or #PAST and TrainSpeed > MINSPEED
Post: / TrainSpeed = MINSPEED
1.9 / Context: / Train::RaiseSpeed()
Inv: / TrainSpeed >=30 and TrainSpeed <=50
Pre: / TrainLocation = #FAR and TrainSpeed < MAXSPEED
Post: / TrainSpeed = MAXSPEED
1.10 / Context: / GateController
Inv:
Inv: / GCState = #PROCESSEXIT implies Gate::GateState =#CLOSED or Gate::GateState = #MOVINGUP
GCState = #PROCESSAPPROACH implies Gate::GateState = #OPENED or Gate::GateState = #MOVINGDOWN
1.11 / Context: / GateController::SendSignal(Signal)
Inv: / Signal = #LOWER or Signal = #RAISE
Pre: / GCState = #PROCESSAPPROACH or
GCState = #PROCESSEXIT
Post: / If Signal = #LOWER then To Gate send ProcessEvent(#LOWER) endif
If Signal = #RAISE then To Gate send ProcessEvent(#LOWER) endif
1.12 / Context: / GateController::ProcessEvent(Event)
Inv: / Event = #APPROACH or Event = #EXIT or Event = #OPENED or Event = #CLOSED
Pre: / (GCState = #IDLE and Event = #APPROACH) or
(GCState = #IDLE and Event = #EXIT) or
(GCState = #PROCESSEXIT and Event = #OPENED) or
(GCState = #PROCESSAPPROACH and Event = #CLOSED) or
(GCState = #PROCESSEXIT and Event = #APPROACH) or
(GCState = #PROCESSAPPROACH and Event = #APPROACH) or
(GCState = #PROCESSEXIT and Event = #EXIT) or
(GCState = #PROCESSAPPROACH and Event = #EXIT) or
(GCState = #IDLE and Event = #CLOSED) or
(GCState = #IDLE and Event = #OPENED)
Post:
Post:
Post:
Post:
Post:
Action:
Post
Action:
Post:
Action:
Post:
Action:
Post:
Action:
Post:
Action: / If GCState = #IDLE and Event = #APPROACH then GCState = #PROCESSAPPROACH endif
If GCState = #IDLE and Event = #EXIT then GCState = #PROCESSEXIT endif
If GCState = #PROCESSEXIT and Event = #OPENED then GCState = #IDLE endif
If GCState = #PROCESSAPPROACH and Event = #CLOSED then
GCState = #IDLE endif
If GCState = #PROCESSEXIT and Event = #APPROACH then
GCState = #PROCESSAPPROACH endif
To self send ProcessEvent(#APPROACH)
If GCState = #PROCESSAPPROACH and Event = #APPROACH then
GCState = #PROCESSAPPROACH endif
To self send ProcessEvent(#APPROACH)
If GCState = #PROCESSEXIT and Event = #EXIT then
GCState = #PROCESSEXIT endif
To self send ProcessEvent(#EXIT)
If GCState = #PROCESSAPPROACH and Event = #EXIT then
GCState = #PROCESSAPPROACH endif
To self send ProcessEvent(#EXIT)
If GCState = #IDLE and Event = #CLOSED then
GCState = #IDLE endif
To self send ProcessEvent(#CLOSED)
If GCState = #IDLE and Event = #OPENED then
GCState = #IDLE
To self send ProcessEvent(#OPENED)
1.13 / Context: / Gate
1.13.1
1.13.2
1.13.3
1.13.4 / Inv:
Inv:
Inv:
Inv: / GatePosition = GATEUPPOSITION and GateSpeed = STOPSPEED implies GateState = #OPEN
GatePosition = GATEDOWNPOSITION and GateSpeed = STOPSPEED implies GateState = #CLOSED
GatePosition < GATEUPPOSITION and GatePosition > GATEDOWNPOSITION and GateSpeed = DOWNSPEED implies GateState = #MOVINGDOWN
GatePosition > GATEDOWNPOSITION and GatePosition < GATEUPPOSITION and GateSpeed = UPSPEED implies GateState = #MOVINGUP
1.14 / Context: / Gate::ProcessGateEvent(Event)
Inv: / Event = #LOWER or Event = #RAISE or Event = OPENED or Event = CLOSED
Pre: / (GateState = #OPEN and Event = #LOWER) or
(GateState = #OPEN and Event = #RAISE) or
(GateState = #MOVINGDOWN and Event = #LOWER) or
(GateState = #MOVINGDOWN and Event = #RAISE) or
(GateState = #MOVINGDOWN and GatePosition = GATEDOWNPOSITION and Event = #CLOSED) or
(GateState = #CLOSED and Event = #LOWER) or
(GateState = #CLOSED and Event = #RAISE) or
(GateState = #MOVINGUP and Event = #RAISE) or
(GateState = #MOVINGUP and Event = #LOWER) or
(Event = #OPENED and GateState= #MOVINGUP and GatePosition = GATEUPPOSITION)
Post:
Post:
Action:
Post:
Action:
Post:
Post:
Action:
Post:
Post:
Post:
Action:
Post:
Post:
Action: / If GateState = #OPEN and Event = #LOWER then To self send LowerGate() endif
If GateState = #OPEN and Event = #RAISE then GateState = #OPEN endif
To self send ProcessGateEvent(#RAISE)
If GateState = #MOVINGDOWN and Event = #LOWER then GateState = #MOVINGDOWN endif
To self send ProcessGateEvent(#LOWER)
If GateState = #MOVINGDOWN and Event = #RAISE then To self send RaiseGate() endif
If GateState = #MOVINGDOWN and GatePosition = GATEDOWNPOSITION and Event = #CLOSED then
GateState = #CLOSED endif
To self send SetGateSpeed(STOPSPEED)
If GateState = #CLOSED and Event = #LOWER then
GateState = #CLOSED endif
GateState = #CLOSED and Event = #RAISE then
To self send RaiseGate() endif
If GateState = #MOVINGUP and Event = #RAISE then
GateState = #MOVINGUP endif
To self send ProcessGateEvent(#RAISE)
If GateState = #MOVINGUP and Event = #LOWER then
To self send LowerGate() endif
If Event = #OPENED and GateState= #MOVINGUP and GatePosition = GATEUPPOSITION then GateState = #OPEN endif
To self send SetGateSpeed(STOPSPEED)
1.15 / Context: / Gate::LowerGate()
Inv. / None
Pre: / (GateState = #OPEN or GateState = #MOVINGUP or GateState = #MOVINGDOWN) and Event = #LOWER
Post: / GateState = #MOVINGDOWN
Action: / To self send SetGateSpeed(DOWNSPEED)
1.16 / Context: / Gate::RaiseGate()
Inv: / None
Pre: / (GateState = #CLOSED or GateState = #MOVINGDOWN or GateState = #MOVINGUP) and Event = #RAISE
Post: / GateState =# MOVINGUP
Action: / To self send SetGateSpeed(UPSPEED)
1.17 / Context: / Gate:: SetGateSpeed(Speed)
Inv: / Speed = 0 or Speed = -9 or Speed = 9
Pre: / None
Post:
Action: / GateSpeed = Speed
If GateSpeed = UPSPEED or GateSpeed = DOWNSPEED then to self send MoveGate() endif
1.18 / Context: / Gate::MoveGate()
Inv:
Inv:
Inv:
Inv: / GatePosition >= 0 and GatePosition <=90
GateSpeed = 0 implies GateState = #OPEN or GateState = #CLOSED
GateSpeed = UPSPEED implies GateState = #MOVINGUP
GateSpeed = DOWNSPEED implies GateState = #MOVINGDOWN
Pre: / none
Post:
Action:
Action: / GatePosition = GatePosition@pre +(GateSpeed*GateTravelTime)
If GatePosition = GATEUPPOSITION then
To self send ProcessGateEvent(#OPENED) and
To self send SendSignal(#OPENED) endif
If GatePosition = GATEDOWNPOSITION then
To self send ProcessGateEvent(#CLOSED) and
To self send SendSignal(#CLOSED) endif
1.19 / Context: / Gate::SendSignal(Signal)
Inv: / Signal = #OPENED or Signal = #CLOSED
Pre: / (GateState = #OPEN and Signal = #OPENED) or
(GateState = #CLOSED and Signal = #CLOSED)
Post:
Post: / If GateState = #OPEN and Signal = #OPENED then
To GateController send ProcessEvent(#OPENED) endif
If GateState = #CLOSED and Signal = #CLOSED then
To GateController send ProcessEvent(#CLOSED) endif

Traceability Matrix from Statecharts to OCL

State, Condition, Event Modeled

/ OCL Reference

TRAIN

TrainLocation = FAR when CurrentLocation >EXITLOCATION and < APPROACHLOCATION / 1.2, 1.5, 1.6
TrainLocation = NEAR when CurrentLocation >= APPROACHLOCATION and TrainLocation <=TrackLength / 1.3, 1.5, 1.6
TrainLocation = PAST when CurrentLocation >=GateLocaton and CurrentLocation < ExitLocation / 1.4,1.5, 1.6
When TrainLocation = FAR and CurrentLocation = ApproachLocation Send Approach Signal / 1.9, 1.5
When TrainLocation = PAST and CurrentLocation = ExitLocation Send Exit Signal / 1.5, 1.7
When TrainLocation = NEAR and CurrentLocation = GATELOCATION then TrainLocation transitions to PAST / 1.4, 1.5, 1.7
When TrainLocation = FAR RaiseSpeed to 50 / 1.9
When TrainLocation = NEAR or PAST Reduce Speed to 30 / 1.8

GateController

If the GateController is IDLE and receives an APPROACH event it Processes the APPROACH / 1.12
When GateController processes an APPROACH signal, it sends a LOWER event to the Gate / 1.11
If the GateController is IDLE and receives an EXIT event it Processes the EXIT / 1.12
When GateController processes an EXIT signal, it sends a RAISE event to the Gate / 1.11
When the GateController is processing the APPROACH signal and receives a CLOSED event from the Gate the GateController returns to IDLE / 1.12
When the GateController is processing the EXIT signal and receives an OPENED event from the Gate the GateController returns to IDLE / 1.12
If the GateController is IDLE and recieves a CLOSED or OPENED event, the event is ignored / 1.12
If the GateController is processing an EXIT event and receives another APPROACH event from the TRAIN, the GateController transitions to Processing an APPROACH event / 1.12
If the GateController is processing an APPROACH event and receives another APPROACH event the event is ignored / 1.12
If the GateController is processing an APPROACH event and receives an EXIT event the event is ignored / 1.12
If the GateController is processing an EXIT event and receives an EXIT event the event is ignored / 1.12
The GateController cannot receive a CLOSED event from the Gate when processing an EXIT / 1.10
The GateController cannot receive a OPENED event from the Gate when processing an APPROACH / 1.10

GATE

The Gate is in the MOVINGUP state when the GATEPOSITION < 90 and the GateSpeed = 9 / 1.13.4
The Gate is in the OPEN state when the GATEPOSITION = 90 and the GateSpeed = 0 / 1.13.1
The Gate is in the MOVINGDOWN state when the GATEPOSITION > 0 and the GateSpeed = -9 / 1.13.3
The Gate is in the CLOSED state when the GATEPOSITION = 0 and the GateSpeed = 0 / 1.13.2
The Gate transitions from MOVINGUP to OPEN when GatePosition =90 / 1.14
The Gate transitions from OPEN to MOVINGDOWN when the GATE receives a LOWER signal from the GateController / 1.14
The Gate transitions from MOVINGDOWN to CLOSED when the GATEPOSITION = 0 / 1.14, 1.18
The Gate transitions from MOVINGDOWN to MOVINGUP when the GATE receives a RAISE signal from the GateController / 1.14
The Gate transitions from MOVINGUP to MOVINGDOWN when the GATE receives a LOWER signal from the GateController / 1.14
The Gate transitions from CLOSED to MOVINGUP when the GATE receives a RAISE signal from the GateController / 1.14
If the Gate is in the OPEN state and gets a RAISE event, the event is ignored / 1.14
If the Gate is in the CLOSED state and gets a LOWER event, the event is ignored / 1.14
If the Gate is in the MOVINGDOWN state and gets a LOWER event, the event is ignored / 1.14
If the Gate is in the MOVINGUP state and gets a Raise event, the event is ignored / 1.14
The Gate cannot directly transition from OPEN to CLOSED, it must first transition to MOVINGDOWN / 1.14, 1.15
The Gate cannot directly transition from CLOSED to OPEN, it must first transition to MOVINGUP / 1.14, 1.16
GatePosition is continuously calculated while the Gate is MOVINGUP or MOVINGDOWN based upon the time and speed of the lower/raise / 1.18
The Gate sends an OPENED signal to the GateController when the Gate transitions from MOVINGUP to OPEN / 1.19
The Gate sends an CLOSED signal to the GateController when the Gate transitions from MOVINGDOWN to CLOSED / 1.19
GateSpeed is adjusted when a LOWER or RAISE or OPENED or CLOSED event occurs. / 1.17