94 GUI design
Chapter 14
Assumptions and invariants
This chapter lists the assumptions and invariants identified for the system to work. This list of invariants and assumptions is a summary of the decisions made in chapters 10 and 9.
1. It is assumed that TCCs and SBCCs can communicate using some existing communication service like a GSM network.
2. It is assumed that a TCC knows it’s current position by either measuring length from last station or using GPS.
3. It is assumed that trains cannot collide when inside and ESA.
4. It is assumed that SBs have some interface to existing sensory equipment on the track.
5. The distance from a segment border to a reservation point must be less than the length of the segment (rp < segment.length)
6. The brake point must be closer to the segment border than the reservation point (rp > bp).
7. The train must not be on two segments when crossing a reservation point (rp < segment.length−train.length)
8. At the most, a train can be on two segments at a time. This means that the train must be shorter than any segment (train.length < segment.length).
9. The length of the shortest train must be longer than the largest possible collision detection error (scol< train.lengthmin)
10. A train must be able to stop before entering the next segment when it starts braking at the brake point. Therefore this length has to be longer than the max brake length + the max simulation error made by discrete time updates (bp > sbrk+serr).
96 Assumptions and invariants
11. A train must be able to brake entirely in an ESA (ESA.length > bp).
12. The TCC must handle the error made by discrete time updates (vtrain+ verr< vmax)
Chapter 15
RSL modelling method summary
This chapter briefly lists the method used to develop the model in the following chapters. This is not a general description of transformation of RSL models so all trivial steps are left out and only changes specific to this system / model are listed.
For a model-specific description of the modules, their function, and the devel-opment of the model in this project please refer to chapter 16.
For a more detailed and general description of RSL model transformations / refinements please refer to appendix B.
The model is constructed to satisfy two conditions:
1. Suitable for easy translation into JAVA. Therefore the use of RSL spe-cialties like subtypes - which are not directly implementable in JAVA - is minimized as much as possible.
2. Structured for proving safety. Therefore axioms and invariant predicates are added indicating what should hold for this system. To see the theory of how to use these predicates to prove safety please refer to chapter 23.
15.1 Initial specification
This section describes the development of the initial abstract specification.
In this phase all modules (schemes) are flat specifications. This means that no object oriented structure is used yet. All modules define a main type on which all functions in the module are based. One exception though, is the Types
98 RSL modelling method summary
module which is only a utility module.
15.1.1 Initial model overview
Figure 15.1 shows an illustration of the schemes of the initial model. The arrows indicate which schemes are parameterized by other schemes.
Figure 15.1: Initial model structure
15.1.2 Types
A Types module is defined which contains all common types for all modules.
The types module also contains utility functions that only operates on types defined in the Types module itself. All other modules is parameterized by this module.
15.1.3 Statics
This scheme defines the static physical aspects of the system.
• This scheme is parameterizedby theTypes module.
schemeStatics(T : Types)
• Thetype of interestcontains the entire static system configuration.
15.1 Initial specification 99
type
Configuration
• Aconstantcontaining the actual configuration instance is defined. This is necessary to be able to express some properties of the actual configuration instance.
value
conf : Configuration
• Functions that extract information (observers) from the main configu-ration type are added.
value
obsi: Tj×..×Configuration→Tn
• Wellformedness requirementsare defined in terms of a boolean func-tion (predicate). The wellformedness predicate defines all the constraints of a wellformedConfigurationtype. This predicate is based on proper-ties observed by observer functions defined above. The predicate defines the relationship between the observer functions.
value
is wf : Configuration→Bool is wf(con)≡p(..,obsi(..,con))
• Anaxiomis added stating that the configuration instanceconf must be wellformed. This represents that a configuration loaded from an external supplier - such as a XML file - must be checked for wellformedness before use.
axiom [ conf is wf ]
is wf(conf)
15.1.4 Dynamics
This scheme defines the dynamic physical aspects of the system.
• The scheme isparameterizedwith theStatics andTypes schemes.
schemeDynamics(T : Types, S : Statics(T))
100 RSL modelling method summary
• Thetype of interestcontains the composite state of the entire physical system.
type State
• A constantsymbolizing theinitial stateof the system is defined. This is necessary to be able to express some properties of this state.
value
initState : State
• Observerand generator functionsare defined to be able to extract / change information in the main type.
value
obsi: Tk ×..×State→Tn, geni: Tk×..×Tn×State→State
• Wellformedness requirementsis defined in terms of a predicate based on the observer functions. This predicate also needs a configuration as input because the dynamic properties are based on the static domain.
Therefore a state is only wellformed if the underlying static configuration is wellformed.
value
is wf : State×S.Configuration→Bool is wf(s,con)≡S.is wf(con)∧p(..,obsi(..,s))
• Some requirements for the initial stateof the system are - like the well-formedness predicate - defined as a predicate based on the observer func-tions. This predicate includes the wellformedness requirements. This also needs a configuration as input.
value
init req : State×S.Configuration→Bool init req(s,con)≡is wf(s,con)∧p(..,obsi(..,s))
• A predicate saf e is also defined. This predicate defines what a safe physical state is. This is usually the fact that no entities arecollidingor derailing(in the railway domain). This predicate also includes theis wf predicate.
value
safe : State×S.Configuration→Bool safe(s,con)≡is wf(s,con)∧p(..,obsi(..,s))
15.1 Initial specification 101
• Observer/generator axioms are added to define the relationship be-tween these. Preconditionsfor the observers and generators are added to the observer generator axioms.
axiom [ obsigenj]
obsi(..,genj(..,s))≡val expr preprecondj(...)
• Axioms are added stating thatgenerators preserves wellformedness if the preconditions are satisfied.
axiom
[ wf pres geni]
∀s : State,
con : S.Configuration•
is wf(s,con)∧precondi(..)⇒is wf(geni(..,s)))
• An axiom is added requiring theinitial state to satisfy the initial state requirements. The constantS.conf is used as parameter.
axiom
[ init state req ]
init req(initStat,S.conf)
15.1.5 Control
This scheme defines the state of the entire control system.
• The scheme isparameterizedby theTypes module, theStaticsmodule, and theDynamics module.
schemeControl(T : Types, S : Statics(T), D : Dynamics(T,S))
• Atype of interestis defined to contain the entire control system state.
type
ControlState
• Aconstantis defined to represent the initial state of the control system.
value
initControlState : ControlState
102 RSL modelling method summary
• Observerandgenerator functions are defined to extract / change in-formation in the main type.
value
obsi: Tk ×..×ControlState→Tn,
geni: Tk×..×Tn×ControlState→ControlState
• A wellformedness predicate is defined for the control state. For a control state to be wellformed both configuration and dynamic state must also be wellformed.
value
is wf : ControlState×D.State×S.Configuration→Bool is wf(cs,ds,con)≡D.is wf(ds,con)∧p(..,obsi(..,cs))
• A predicateconsistentis defined. It defines the relationship between the physical state and the control state, and perhaps some safety measures which only concern the physical state.
value
consistent : ControlState×D.State×S.Configuration→Bool consistent(cs,ds,con)≡is wf(cs,ds,con)∧p(..,obsi(..,cs))
• A predicateinit reqdefines the requirements for the initial control state.
value
init req : ControlState×D.State×S.Configuration→Bool init req(cs,ds,con)≡is wf(cs,ds,con)∧p(..,obsi(..,cs))
• An axiom is added stating that theinitial statemust satisfy theinit req predicate.
axiom
init req(initControlState,D.initState,S.conf)
• Observer / generator axioms are added defining the relationship be-tween observers and generators. Preconditions are also added to these axioms.
axiom [ obsigenj]
∀cs : ControlState•
obsi(..,genj(..,cs))≡val expr preprecondj(..)