System Specification Document

System Definitions [ Definitions of the System ]

1. Purpose of the system

Specification:

The purpose of the system is to connect two environments:
internal space with atmosphere (boat) and external water environment (sea).

The system is composed of lock chamber with 
two lock-gates. The lock chamber has space for one unit.

When units are locked (both gates are closed) in chamber,
the water pump starts to pump out (or to pump up) water 
in a lock chamber.

When pressure will be balanced, corresponding lock-gate opens
and units leave the lock chamber.

Maybe system must support movement detection!

Picture:

2. Conventions

Specification:

All requirements to the system must be coded.
The code pattern:
 LCR(Number).

Example
 LCR(1)
 LCR(2)
etc.

Properties must be coded by following pattern:
 LCP(Number).

3. States description

Specification:

Initial state.
 Lock chamber is locked.
 Air is in the lock chamber.
 No unit is in the lock chamber.
 Water pump is stopped. 
 No door request.
 State is free.

Initial state == Door request (Door) ==> Open for entrance (Door).
Open for entrance == Unit entered ==> Balancing pressure.
Balancing pressure == Time ==> Open for leave
Open for leave == Unit is leaving ==> Blocking the chamber.
Blocking the chamber == Automatic Control System ==> Initial state.

Specifications [ Formal Specification of the system ]

1. LCR(1). Base notions

2. LCR(2). Initial State

Specification:

The specification of the system's 
 intial state.

3. LCR(3). State1

Specification:

Specifications of the system states and
 transitions between them.

4. LCR(4). State2

5. LCR(5). State3

6. LCR(6). State4

7. LCR(7). State5

8. LCR(8). State6

9. LCR(9). State7

10. LCR(10). State8

11. LCR(11). State9

12. LCR(12). State10

13. LCR(13). State11

14. LCR(14). State12

15. LCR(15). State13

16. LCR(16). State14

17. LCR(17). State15

18. LCR(18). State16

Properties [ Properties of the give specifications ]

1. LCP(1). Water pump

Specification:

The water pump must operate only when lock chamber 
is locked. e.g. both doors are closed.

In other case it will cause flooding.

Prepared by Easy Requirements Environment, Date: Wed Nov 08 20:27:23 EET 2006