a) The elevator system shall accept passenger requests and provide feedback.
b) The elevator system shall support all relevant fire and safety codes in effect.
c) The elevator system shall have an MTBF (Mean Time Between Failures) of greater than 1 year.
d) The elevator system shall provide alternate exit(s) in the event that the primary exit is inoperable.
e) The elevator system shall receive 99.99% of passenger activated floor selections in each elevator car.
f) The elevator system shall provide rates of acceleration and deceleration that are within the standard limits of comfort to passengers.
Below is an example of what is being requested:
Express the following set of requirements with First Order Logic, and define terminology (predicates and functions to be used) in tables.
A predicate is used to represent a relation; a function is a mapping from one domain to another.
- The elevator system shall strictly adhere to all Federal, State, and Local government regulations.
Fine-grained representation, (which is more general and having fewer new predicates to be defined, thus more appreciated):
Alternatively, a coarse-grained representation, (which needs to define many ad hoc predicates and functions; still, acceptable)
- The elevator system shall receive 99% of signals from the passengers to control operation of the elevator car doors.
- The elevator system shall receive 50% of all repairs within 2 hours.
- The elevator system shall receive 50% of all routine maintenance actions within 1 hour.
- The elevator system shall have an MTTR (Mean Time To Recover) of less than 8 hours.
Terminology Table (Predicate)
Predicate Definition IsA(x,y) x is a y. IsFrom(x,y) x is from y. ComplyTo(x,y) x complies to y. IsRegulationOf(x,y) x is a regulation of y. (This is a coarse-grained representation. If only fine-grained representation is used, this predicate is not needed.) PartOf(x,y) x is a part of y. (Same as the part property in bdd of SysML) Control(x,y) x controls y. GE(x,y) x is greater than or equals to y. LT(x,y) x is less than y. ApplyTo(x,y) x is applied to y. StartAT(x,t) x starts at time point t. FinishAT(x,t) x finishes at time point t. DetectedAT(x,t) x is detected at time point t.
Function Definition probOf(x) The probability of x; x is of Boolean type. less(x,y) x is than y -- a Boolean function. receive(x,y) x receives y – a Boolean function. subtract(x,y) x subtracts y timePeriod(x,y) A time period of quantity x and unit in y.