NED University of Engineering & Technology

Department of Software Engineering

Complex Engineering Problem

Smart Light Automation System for Hospitals

Group members:

➢ Sadia Khan (SE-22003)

➢ Kanza Muhammad Akram (SE-22024)
➢ Syed Arham Hasan (SE-22039)

Course Title: Formal Methods in Software Engineering

Submitted to: Sir Mustafa Latif

1
Introduction & Overview
The Smart Light Automation System for Hospitals is a lighting solution designed to optimize energy use, improve patient
comfort, and streamline lighting management in healthcare facilities.

This system uses automation, passive infrared sensors (PIR) for motion detection, QR code-based device registration,
and an intuitive control interface to ensure that lighting is perfectly adapted to each room's needs, contributing to a more
efficient and comfortable hospital environment.

The Smart Light Automation System for Hospitals is a safety-critical system because it directly affects patient safety
and comfort. Key critical areas include:

1. Lighting Intensity and Timing: Any malfunction here can cause patient stress and interfere with recovery.
Improper lighting could disrupt the healing process, especially for sensitive patients.
2. Emergency Lighting: Failure of emergency lighting could delay critical medical interventions, potentially
jeopardizing patient health during emergencies.
3. Sensor Reliability: Failures in PIR sensors may create dark spots, exposing patients, especially those with
limited mobility, to a higher risk of falls. This is particularly dangerous in healthcare environments where patient
movement is restricted.
4. Control System Security: Unauthorized access to the system can result in disruptions in critical areas, such as
operating rooms or ICUs. Additionally, QR code vulnerabilities could compromise the hospital's broader network,
leading to security risks.
5. Maintenance and Response Time: Delays in addressing system malfunctions could further impair care in high-
dependency units, where precise lighting control is essential for patient safety.

Smart Light Automation System Requirements

1. Functional Requirements
For example, lights can dim slightly when no significant motion is detected, but
1.1. User Management users can override this via manual control.

● Users should be able to turn lights on or off in specific rooms.

● Users should be able to control the intensity (brightness) of the lights (e.g., dimmer function).
● The system must allow user to add roomName and scan light QR code to add light into the system
● The system must allow users to add passive infrared sensors through QR code scanning.

1.2. Lighting Controller

● The system should support passive infrared sensors to automatically turn lights on/off when a person is
detected or not detected in a room.
● The system should change the light mode “on/off” when requested by the user.
● The system must check the current light status before changing its state.
● The system should set the brightness as requested by the user.
● The system must check the brightness range of specific light before processing the user request.
● The system must ensure that all lights in the specified room are added to the hashmap.

2
1.3. Room Management

● Users should be able to assign lights to specific rooms through a simple interface, ensuring that each light
is appropriately categorized and can be controlled within the right context.
● Rooms must be added with a unique name and should allow for a flexible and scalable system where users
can add multiple rooms to their profile.
● Users should be able to modify room settings, such as renaming or removing rooms if necessary.

1.4. Motion Detection & Automation

● Passive Infrared Sensors (PIR) should automatically detect the presence or absence of people in a room,
triggering light operations accordingly.
● If motion is detected, the system will turn the lights on in the room, provided the room’s light is in an off
state.
● If no motion is detected within a specified period, the system should automatically turn the lights off to
conserve energy.
● System should provide an option to disable automatic motion-triggered control in specific rooms if the user
prefers manual control.
yr yeh batao ke agr user khud manual intervention se light on/off karsakta hai
then PIR ki kya need hai for turning light on/off through motion detection

3
System Architecture Design:4+1 VIEW MODEL

1. Logical View: A LightController can manage multiple Rooms

A
LightCon
troller
can
handle
requests
from
multiple
Users

A PassiveInfraredSensor interacts with a

The LightController sets the status (on/off)
LightController to enable person
and brightness levels for individual lights
detection and trigger light control
operations.

A Room contains a list of Light objects

1. User
● Represents hospital staff (e.g., nurses, maintenance) who manage room lights.
● Can turn lights on/off, adjust brightness, and scan a QR code to identify a specific light.
● Manages a list of controlled lights by room for quick access.

2. Light
● Each light has a unique ID, brightness settings, and a QR code for identification.
● Can be turned on/off and have its brightness adjusted according to area requirements (e.g., dim for resting rooms,
bright for hallways).

3. LightController
4
 ● Central control system for managing all lights.
● Monitors which lights are on/off, their brightness levels, and occupancy status.
● Adjusts lights automatically based on room occupancy, time of day, and staff settings.

4. PassiveInfraredSensor
● Detects room occupancy by sensing movement or presence.
● Assigned to specific rooms to signal the LightController when someone enters or exits.

5. Room
● Groups lights within each specific room (e.g., patient rooms, hallways).
● Makes it easier for staff to manage all lights in a room collectively.
● Maintains a list of lights it contains, allowing the LightController to manage lighting for each room effectively.

Enumeration

• ON: Turns on lights in a specific room when movement is detected, e.g., a nurse entering a patient’s room.
• OFF: Turns off lights when a room is empty, conserving energy.
• INCREASE BRIGHTNESS: Increases light brightness, useful for procedures or tasks requiring more visibility.
• DECREASE BRIGHTNESS: Lowers brightness, e.g., at night or when patients need rest.
• PERSON DETECTED: Signals the presence of someone in the room, prompting the lights to turn on or adjust
brightness accordingly.

5
2. Process View

I. User Management

Explanation:

1. The user scans the light to add it to the system.

2. The system then prompts the user to enter the room name, and the user provides the name of the room.
3. If the user wants to turn on the light, they request the system to do so, and the system turns the light on.
4. Once the light is on, the user is given the option to control the brightness.
5. The user enters a brightness value, and the system validates whether the brightness is within the acceptable
range. If the value is valid, the system sets the brightness accordingly.
6. If the user requests to turn off the light, the system turns off all lights in the room.

6
ii. Lighting Controller

Explanation:
1. The user selects a room to control its lights.
2. The user selects a specific light to control (turn on/off or adjust brightness).
3. If the user wants to turn on the lights, they click a button to turn on the light.
4. The system sends a request to the lighting controller to turn on the light.
5. The lighting controller turns on the specified light and sends a response back to the system, confirming the
request was fulfilled.
6. The system shows a message to the user indicating that the light is on.
7. If the user wants to adjust the brightness after the light is on, they can adjust the brightness through the
system.
8. The system sends a request to the lighting controller to adjust the brightness.
9. The lighting controller adjusts the brightness and sends a response back to the system, confirming the
request was fulfilled.
10. The system displays a message to the user indicating that the brightness has been adjusted.
11. If the user wants to turn off the light, they click the button to turn off the light in the system.
12. The system sends a request to the lighting controller to turn off the light.
13. The lighting controller turns off the light and sends a response back to the system, confirming the request
was fulfilled.
14. The system displays a message to the user indicating that the light is off.

7
iii) Automated Lighting Control

Explanation:
1. The Passive Infrared Sensor monitors temperature continuously to detect a person’s presence.
2. If a temperature change is detected within a specified range, it indicates a person is present.
3. The sensor sends a "Person Detected" signal to the system.
4. The system requests the Lighting Controller to turn on the lights.
5. The Lighting Controller activates the lights in the room.
6. If no temperature change is detected, it indicates the room is empty.
7. The sensor sends a "No Person Detected" signal to the system.
8. The system requests the Lighting Controller to turn off the lights.
9. The Lighting Controller turns off the lights to save energy.

8
3. Development View

I. Component Diagram:

EXPLANATION:
The above developmental view represents The hospital lighting system that automates control using various components
that work together. The SystemDatabase stores data on users, lights, and rooms, while the UserInterface allows hospital
staff to interact with the system. UserManagement handles permissions, and the LightControlModule adjusts lights based
on user commands or sensor input. Passive Infrared Sensors detect room occupancy, triggering automatic light adjustments
through the AutomatedLightControlModule, which then controls SmartLights based on presence or user instructions.
In this component diagram the components are dependent over one another to get the necessary information to carry out the
proper functionality of the proposed system.

9
4. Physical View:

I. Deployment Diagram:

Explanation:

1. Smart Light Controlling System Node: Manages core functions:

● User Management: Handles user login, access, and interactions.
● Light Controller: Controls lights, turning them on/off and adjusting brightness.
● Room Management: Configures rooms, light settings, and assigns sensors.
● Communicates with the Database Server Node for data and Physical Devices Node for light control.
2. Database Server Node: Central storage for:
● User Data: User information and permissions.
● Lights Data: Status and settings of lights.
● Room Data: Room details, configurations, and light assignments.
● Sensor Data: Occupancy data from infrared sensors.
3. Physical Devices Node: Contains hardware components:
● Lights: Respond to control commands.
● Sensors: Detect presence for automatic lighting.
● Receives commands from the Smart Light Controlling System Node based on inputs or sensor events.

10
5. Scenario View (+1 view):

I. Usecase Diagram:

EXPLANATION

1. Scan and Add Light to Room: The user scans the QR code on a light to register it to a specific room, making it
controllable via the interface.
2. Turn On Light: Once registered, the user can turn on the light remotely, setting its status to "on" through any
connected device.
3. Turn Off Light: The user can turn off the light from any device in the system, setting it to "off" to save energy.
4. Set Brightness of Light: The user adjusts the brightness level to fit room needs, with the system ensuring the
selected brightness is within the light's range.

11
 VDM-SL Specification with Class Diagram

Translating the Signal Type

VDM-SL
types
Signal = <ON> | <OFF> | <INCREASE_BRIGHTNESS> | <DECREASE_BRIGHTNESS> | <PERSON_DETECTED>

JAVA CODE
public class Signal {
private int value;
// Class constants representing the different signals
public static final Signal ON = new Signal(0);
public static final Signal OFF = new Signal(1);
public static final Signal INCREASE_BRIGHTNESS = new Signal(2);
public static final Signal DECREASE_BRIGHTNESS = new Signal(3);
public static final Signal PERSON_DETECTED = new Signal(4);

// Private constructor to prevent external instantiation

private Signal(int value) {
this.value = value;
}
// Overridden equals method for comparing Signal instances
This method overrides the default equals method to compare Signal
public boolean equals(Object objectIn) { objects.
if (this == objectIn) It checks if the objectIn has the same value as the current Signal object.
this == objectIn checks if they refer to the exact same instance.
return true; If not, it casts the object to Signal and compares the internal value.

Signal signal = (Signal) objectIn;

return value == signal.value;
}
// toString method to return the name of the current signal
public String toString() {
switch (value) {
case 0:
return "ON";
case 1:
12
 return "OFF";
case 2:
return "INCREASE_BRIGHTNESS";
case 3:
return "DECREASE_BRIGHTNESS";
case 4:
return "PERSON_DETECTED";
default:
return "UNKNOWN";
}
}
}

1. Light

VDM-SL

state Light of
QRCode : seq of char . Understanding cb
cb: It appears to represent the current brightness of the light.
lightID : N This is inferred from the name and its connection to brightness-related conditions (e.g.,
inRange(cb)).
maxBrightness: N It is likely a numeric value (e.g., an integer or real number) that tracks the brightness level
minBrightness: N of the light.
2. Explanation of the VDM Code
lightStatus: B Invariant (inv)
The invariant defines constraints or conditions that the Light object must satisfy at all
currentBrightness: N times.

inv mk-Light(cb) defined as inRange(cb):

inv mk-Light(cb) defined as inRange(cb) mk-Light(cb) is the constructor for the Light type, where cb is the brightness parameter.
inv mk-Light(cb) △ inRange(cb) inRange(cb) is likely a predicate (a boolean function) that checks whether the brightness
cb is within a valid range.
Example: inRange(cb) = cb >= 0 and cb <= maxBrightness.
The invariant ensures that the brightness value cb remains valid whenever a Light object
init mk-Light(cb) △ cb = maxBrightness*0.8 is created or modified.
Alternate Notation:
end
inv mk-Light(cb) inRange(cb):
The symbol is equivalent to defined as. Both indicate the invariant is defined by the
functions condition inRange(cb).
Initialization (init)
inRange(val:N) result:B The initialization clause defines the initial state of a Light object when it is created.

pre TRUE init mk-Light(cb) cb = maxBrightness * 0.8:

When a Light object is initialized, the cb (current brightness) is set to 80% of the maximum
post result <=> minBrightness <= val <= MaxBrightness brightness (maxBrightness).
This ensures that the light starts with a predefined brightness level.

operations
-- to set the current light status
13
setLightStatus()
ext wr lightStatus: B
pre TRUE
post lightStatus = ~lightStatus

-- to get the current light status

getLightStatus() status : B
ext rd lightStatus : Z
pre TRUE
post status = lightStatus

-- to set brightness of light

setBrightness(brightness: N)
ext wr currentBrightness: N
pre inRange(brightness) ^ currentBrightness != 0
post currentBrightness = brightness

-- to get the current brightnesss

get Brightness () result: Z
ext rd currentBrightness : Z
pre TRUE
post result = currentBrightness;

-- to get the max brightness of light

get MaxBrightness () result: Z
ext rd maxBrightness : Z
pre TRUE
post result = maxBrightness;

-- to get the min brightness of light

get MinBrightness () result: Z
ext rd minBrightness : Z
pre TRUE
post result = minBrightness;

VDM to JAVA
public class Light {
private String QRCode;
private int lightId;
private int maxBrightness;
private int minBrightness;
private boolean lightStatus;
private int currentBrightness;

public Light(String qrCode, int lightID, int maxBrightness, int minBrightness) {

14
 this.QRCode = qrCode;
this.lightId = lightID;
this.maxBrightness = maxBrightness;
this.minBrightness = minBrightness;
this.lightStatus = false;
this.currentBrightness = (int) (maxBrightness * 0.8);

// Validate the initial brightness within range

if (!inRange(this.currentBrightness)) {
throw new IllegalArgumentException("Initial brightness is out of range.");
}
}
private boolean inRange(int value) {
return minBrightness <= value && value <= maxBrightness;
}
public void setLightStatus() {
this.lightStatus = !this.lightStatus;
}
public boolean getLightStatus() {
return this.lightStatus;
}
public void setBrightness(int brightness) {
if (inRange(brightness) && currentBrightness != 0) {
this.currentBrightness = brightness;
} else {
throw new IllegalArgumentException("Initial brightness is out of range.");
}
}
public int getBrightness() {
return this.currentBrightness;
}
public int getMaxBrightness() {
return this.maxBrightness;
}

public int getMinBrightness() {

return this.minBrightness;
}
};

2. PassiveInfraredSensor

VDM SL:
types

15
Signal = <ON> | <OFF> | <INCREASE_BRIGHTNESS> | <DECREASE_BRIGHTNESS> | <PERSON_DETECTED>
state PassiveInfraredSensor of
sensorID : N
roomName : seq of char
isPersonDetected: B
temp : Z
end

operations
-- to detect Person
detectPerson() signalOut:Signal
ext wr isPersonDetected: B
pre temp > 20 ^ temp < 40
post isPersonDetected = true ^ SignalOut = <PERSON_DETECTED>

VDM to JAVA
public class PassiveInfraredSensor {
private int sensorID;
private String roomName;
private boolean isPersonDetected;
private int temp;

public PassiveInfraredSensor(int sensorID, char roomName, int temp) {

this.sensorID = sensorID;
this.roomName = roomName;
this.isPersonDetected = false;
this.temp = temp;
}

public Signal detectPerson() {

Signal signalOut = Signal.OFF

if (temp > 20 && temp < 40) {

this.isPersonDetected = true;
signalOut = Signal.PERSON_DETECTED;
} else {
isPersonDetected = false;
signalOut = Signal.OFF
}
return signalOut;
}
}

16
3. USER

VDM SL:

types
Signal = <ON> | <OFF> | <INCREASE_BRIGHTNESS> | <DECREASE_BRIGHTNESS> | <DO_NOTHING>

-- Values
values
MAX_BRIGHTNESS : Z = 100;
MIN_BRIGHTNESS : Z = 0;

-- State Definition
state User of
roomname : char;
brightness : Z = 0;
lights : set of Light; -- Set of Light for uniqueness
roomLights : (char -> set of Light); -- Mapping of room names to sets of lights

inv mk_User(roomname, brightness, lights, roomLights) Δ

(brightness >= MIN_BRIGHTNESS ^ brightness <= MAX_BRIGHTNESS ^
roomname ≠ "" ^ lights ≠ nil ^ roomLights ≠ nil);

init mk_User(roomname, brightness, lights, roomLights) Δ

(roomname = "" ^ brightness = 0 ^ lights = nil ^ roomLights = nil);

end User;

-- Functions
functions
-- Check if brightness is within defined range
inRange(brightness : Z) result : B
pre TRUE
post result <=> (brightness >= MIN_BRIGHTNESS ^ brightness <= MAX_BRIGHTNESS);

-- Check if the light ID is valid for the specified room

17
 isLightValid(roomName: char, lightId: N) : B
pre roomName in set dom(roomLights) -- Ensure roomName exists in roomLights mapping
post result <=> (lightId in set roomLights(roomName));

-- Operations
operations
-- Turns on the specified light in the given room if it is currently off
turnOnLights(roomName: char, lightId: N) signalOut: Signal
ext wr roomLights: (char -> set of Light) -- Mapping of room names to sets of lights
pre roomName in set dom(roomLights) ^ isLightValid(roomName, lightId) -- Check if the room exists and the light ID is valid
post (roomLights(roomName)(lightId) = <OFF> =>
roomLights(roomName)(lightId) = <ON> ^ signalOut = <ON>) ^
(roomLights(roomName)(lightId) = <ON> =>
roomLights(roomName)(lightId) = <ON> ^ signalOut = <ON>); -- Explicitly state that it remains ON

-- Turns off the specified light in the given room if it is currently on

turnOffLights(roomName: char, lightId: N) signalOut: Signal
ext wr roomLights: (char -> set of Light) -- Mapping of room names to sets of lights
pre roomName in set dom(roomLights) ^ isLightValid(roomName, lightId) -- Check if the room exists and the light ID is valid
post (roomLights(roomName)(lightId) = <ON> =>
roomLights(roomName)(lightId) = <OFF> ^ signalOut = <OFF>) ^
(roomLights(roomName)(lightId) = <OFF> =>
roomLights(roomName)(lightId) = <OFF> ^ signalOut = <OFF>); -- Explicitly state that it remains OFF

-- Sets the brightness of the lights to a new value, adjusting the signal accordingly
setBrightness(newBrightness: Z) signalOut: Signal
ext wr brightness: Z
pre inRange(newBrightness) -- Ensure the new brightness value is within the defined range
post brightness = newBrightness ^
(newBrightness > brightness ^ signalOut = <INCREASE_BRIGHTNESS> v
newBrightness < brightness ^ signalOut = <DECREASE_BRIGHTNESS> v
newBrightness = brightness ^ signalOut = <DO_NOTHING>); -- Signal the type of adjustment made

-- Scans a QR code for a light in the specified room and adds it to the room's light collection if not already present
scanLightsQRCode(roomName: char, lightID: char)
ext wr roomLights: (char -> set of Light) -- Mapping of room names to sets of lights
pre roomName in set dom(roomLights) -- Ensure roomName exists in roomLights
post lightID not in set roomLights(roomName) =>
roomLights = roomLights ^ {roomName -> roomLights(roomName) U {lightID}}; -- Add the new light ID to the room's set

VDM TO JAVA
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
18
import java.util.Set;
// Enum for different signals
enum Signal {
ON,
OFF,
INCREASE_BRIGHTNESS,
DECREASE_BRIGHTNESS,
DO_NOTHING
}
public class SmartLightSystem {
// Constants for brightness limits
public static final int MAX_BRIGHTNESS = 100;
public static final int MIN_BRIGHTNESS = 0;
// User class definition
public static class User {
private String roomName;
private int brightness;
private Set<Light> lights;
private Map<String, Set<Light>> roomLights;
// Constructor
public User(String roomName, int brightness, Set<Light> lights, Map<String, Set<Light>> roomLights) {
this.roomName = roomName;
this.brightness = brightness;
this.lights = lights;
this.roomLights = roomLights;

// Invariant check
if (!isValidUser()) {
throw new IllegalArgumentException("Invalid User state.");
}
}

// Method to check if the user is in a valid state

private boolean isValidUser() {
return brightness >= MIN_BRIGHTNESS && brightness <= MAX_BRIGHTNESS &&
!roomName.isEmpty() && lights != null && !lights.isEmpty() &&
roomLights != null && !roomLights.isEmpty();
}

// Method to set the brightness and return the corresponding signal

public Signal setBrightness(int newBrightness) {
if (!inRange(newBrightness)) {
throw new IllegalArgumentException("Brightness out of range.");
}

19
 int previousBrightness = this.brightness;
this.brightness = newBrightness;

// Return the corresponding Signal based on the brightness change

if (newBrightness > previousBrightness) {
return Signal.INCREASE_BRIGHTNESS;
} else if (newBrightness < previousBrightness) {
return Signal.DECREASE_BRIGHTNESS;
} else {
return Signal.DO_NOTHING;
}
}
// Helper method to check if brightness is within valid range
private boolean inRange(int brightness) {
return brightness >= MIN_BRIGHTNESS && brightness <= MAX_BRIGHTNESS;
}
}

// Room class definition

public static class Room {
private String roomName;
private Set<Light> lights;
// Constructor
public Room(String roomName, Set<Light> lights) {
this.roomName = roomName;
this.lights = lights;

// Invariant check
if (!isValidRoom()) {
throw new IllegalArgumentException("Invalid Room state.");
}
}

// Method to check if the room is in a valid state

private boolean isValidRoom() {
return !roomName.isEmpty() && lights != null && !lights.isEmpty();
}
}
// Light class definition
public static class Light {
private String id; // Light ID
private boolean isOn;

20
 public Light(String id) {
this.id = id;
this.isOn = false; // Initially off
}
public String getId() {
return id;
}
public boolean isOn() {
return isOn;
}
public void turnOn() {
isOn = true;
}
public void turnOff() {
isOn = false;
}
}
// Function to check if the light ID is valid for the specified room
public static boolean isLightValid(String roomName, String lightId, Map<String, Set<Light>> roomLights) {
return roomLights.containsKey(roomName) && roomLights.get(roomName).stream().anyMatch(light ->
light.getId().equals(lightId));
}
// Operations for turning the light ON/OFF
public static Signal turnOnLight(String roomName, String lightId, Map<String, Set<Light>> roomLights) {
if (!roomLights.containsKey(roomName) || !isLightValid(roomName, lightId, roomLights)) {
throw new IllegalArgumentException("Invalid room or light ID.");
}
Set<Light> lights = roomLights.get(roomName);
for (Light light : lights) {
if (light.getId().equals(lightId) && !light.isOn()) {
light.turnOn();
return Signal.ON;
}
}
return Signal.DO_NOTHING;
}
public static Signal turnOffLight(String roomName, String lightId, Map<String, Set<Light>> roomLights) {
if (!roomLights.containsKey(roomName) || !isLightValid(roomName, lightId, roomLights)) {
throw new IllegalArgumentException("Invalid room or light ID.");
}

Set<Light> lights = roomLights.get(roomName);

for (Light light : lights) {
if (light.getId().equals(lightId) && light.isOn()) {

21
 light.turnOff();
return Signal.OFF;
}
}
return Signal.DO_NOTHING;
}
// Function to scan lights QR Code (not related to Signal but added for completeness)
public static void scanLightsQRCode(String roomName, String lightID, Map<String, Set<Light>> roomLights) {
if (!roomLights.containsKey(roomName)) {
throw new IllegalArgumentException("Invalid room name.");
}

Set<Light> lights = roomLights.get(roomName);

// Check if light already exists
if (lights.stream().noneMatch(light -> light.getId().equals(lightID))) {
lights.add(new Light(lightID)); // Add new light
}
}

4. ROOM

VDM SL
-- State Definition
state Room of
roomname : char;
lights : set of Light; -- Set of Light for uniqueness
inv mk_Room(roomname, lights) Δ
roomname ≠ "" ^ lights ≠ nil;
init mk_Room(roomname, lights) Δ
(roomname = "" ^ lights = nil);
end Room;

VDM TO JAVA
import java.util.Set;
public class Room {
private String roomName;
private Set<Light> lights;
// Constructor
public Room(String roomName, Set<Light> lights) {
this.roomName = roomName;
this.lights = lights;
22
 // Invariant check
if (!isValidRoom()) {
throw new IllegalArgumentException("Invalid Room state.");
}
}
private boolean isValidRoom() {
return !roomName.isEmpty() && lights != null && !lights.isEmpty();
}
public String getRoomName() {
return roomName;
}
public Set<Light> getLights() {
return lights;
}
}

5. Light Controller:

VDM SL
types
Signal = <isPersonDetected>

state lightController of
lightId: N
roomName: Char
isPersonDetected: B
Brightness: N
lightStatus: B

function
getLights: char --> seq of lights
getlights(roomName) Δ if roomName ≠ nil
roomName in set dom(roomlights)
then seq of lights

matchLight: N * char -> [Light]

matchLight(lightid) Δ
23
 let lights = getLights(roomName) in
let matchingLight = [light | light in seq of lights & light.lightId = lightId] in
if matchingLight ≠ [] then
matchingLight

operations
-- get current light status
getLightStatus: () ==> B

-- set light mode

setLightMode(lightId: Z, roomName: char)
if light ≠ nil then
setLightStatus()

ext wr roomLights: map char to seq of Light

wr lightStatus: B
pre getLights(roomName) ^ matchLight(lightId)
post lightStatus = ~lightStatus

-- get current light brightness

getLightBrightness() --> N

-- set light brightness

setBrightness(roomName: char , lightId: N, brightness: N)
if lightStatus = true then
setLightBrightness()
ext roomLights: map char to seq of Light
wr Brightness: N
pre getLights(roomName) ^ matchLight(lightId)
post light.brightness = brightness;

personDetection( ispersonDetected: B, roomName: char, roomLights: Hashmap)

let lights = getLights(roomName) in
-- Turn on each light in the room if person is detected
if isPersonDetected then
seq (l | l in lights & (l.lightStatus = true))
ext wr roomLights: map char to seq of Light
wr lightStatus: map N to B
pre
roomName in set dom(roomLights) and
isPersonDetected = true; -- Ensures person is detected before turning on lights
post
-- Ensures all lights in the room are turned on
(forall l in getLights(roomName) @ l.lightStatus = true)

24
VDM to Java
import java.util.HashMap;
import java.util.List;
import java.util.ArrayList;

class LightController {
// HashMap to store lists of lights in each room, with the room name as the key
private HashMap<String, List<Light>> roomLights = new HashMap<>();

// HashMap to store the status (on/off) of each light by its ID

private HashMap<Integer, Boolean> lightStatus = new HashMap<>();
/**
* Retrieves the list of lights for a given room.
* @param roomName The name of the room.
* @return List of lights in the specified room or an empty list if the room has no lights.
*/
public List<Light> getLights(String roomName) {
if (roomName != null && roomLights.containsKey(roomName)) {
return roomLights.get(roomName);
}
return new ArrayList<>(); // Return empty list if roomName is null or room has no lights
}

/**
* Finds lights by their ID within a specified room.
* @param lightId The ID of the light.
* @param roomName The name of the room.
* @return List of matching lights or null if no match found.
*/
public List<Light> matchLight(int lightId, String roomName) {
List<Light> lights = getLights(roomName); // Get all lights in the specified room
List<Light> matchingLight = new ArrayList<>();
for (Light light : lights) {
if (light.lightId == lightId) {
matchingLight.add(light); // Add to matching lights if IDs match
}
}
return matchingLight.isEmpty() ? null : matchingLight; // Return null if no match found
}
/**
* Checks the on/off status of a specific light by its ID.
* @param lightId The ID of the light.
* @return true if the light is on, false otherwise.

25
*/
public boolean getLightStatus(int lightId) {
return lightStatus.getOrDefault(lightId, false); // Default to false if light ID not found
}
/**
* Turns on a specified light in a room by setting its mode.
* @param lightId The ID of the light.
* @param roomName The name of the room.
*/
public void setLightMode(int lightId, String roomName) {
List<Light> lights = matchLight(lightId, roomName); // Find light with the specified ID in the room
if (lights != null) {
for (Light light : lights) {
lightStatus.put(lightId, true); // Set the status to "on" in the HashMap
light.lightStatus = true; // Change the actual light status
}
}
}

/**
get brightness
*/

public void setBrightness(String roomName, int lightId, int brightness) {

if (getLightStatus(lightId)) { // Check if the light is on
List<Light> lights = matchLight(lightId, roomName);
if (lights != null) {
for (Light light : lights) {
light.brightness = brightness; // Set the brightness for the matching light
}
}
}
}
/**
person detection function
*/
public void personDetection(boolean isPersonDetected, String roomName) {
List<Light> lights = getLights(roomName); // Get all lights in the specified room
if (isPersonDetected) {
for (Light light : lights) {
light.lightStatus = true; // Turn on light
lightStatus.put(light.lightId, true); // Update status in HashMap
}
}

26
 }}

TEST CASES AND TESTER CLASS

1. Light
Tester Class

import java.util.Scanner;
import java.util.Scanner;

public class LightTester {

public static void main(String[] args) {
Scanner scanner = new Scanner(System.in);
char choice;

try {
// Generate a new Light object with example values
Light light = new Light("QR123", 1, 100, 0); // QR code, ID, max brightness, min brightness

do {
System.out.println("\n\t\tLight Tester\n");
System.out.println("1. Display light status");
System.out.println("2. Toggle light status");
System.out.println("3. Display current brightness");
System.out.println("4. Set brightness");
System.out.println("5. Display max brightness");
System.out.println("6. Display min brightness");
System.out.println("7. Quit");
System.out.print("Enter choice (1 - 7): ");
choice = scanner.next().charAt(0); // Get the first character of input
System.out.println(); // Blank line

try {
// Process choice
switch (choice) {
case '1':
option1(light);
break;
case '2':
option2(light);
break;
case '3':
option3(light);
break;
case '4':
option4(light, scanner); // Option for setting brightness
break;
case '5':
option5(light);
break;
case '6':
option6(light);
27
 break;
case '7':
System.out.println("Exiting...");
break;
default:
System.out.println("Invalid choice. Please enter a number between 1 and 7.");
break;
}
} catch (IllegalArgumentException e) {
// Handle out-of-range brightness or other illegal arguments
System.out.println("Error: " + e.getMessage());
}
} while (choice != '7');

} catch (IllegalArgumentException e) {
// Handle initial object creation errors
System.out.println("Initial object setup failed: " + e.getMessage());
} finally {
scanner.close(); // Close the scanner to avoid resource leaks
}
}

// Display light status

public static void option1(Light light) {
System.out.println("Light is currently " + (light.getLightStatus() ? "ON" : "OFF"));
}

// Toggle light status

public static void option2(Light light) {
light.setLightStatus();
System.out.println("Light status toggled. Now it is " + (light.getLightStatus() ? "ON" : "OFF"));
}

// Display current brightness

public static void option3(Light light) {
System.out.println("Current brightness is: " + light.getBrightness());
}

// Set brightness within range

public static void option4(Light light, Scanner scanner) {
System.out.print("Enter brightness level within range (" + light.getMinBrightness() + " - " + light.getMaxBrightness() + "): ");
int brightness = scanner.nextInt();

// Explicitly check using the inRange method before setting brightness

if (light.inRange(brightness)) {
light.setBrightness(brightness);
System.out.println("Brightness set to: " + light.getBrightness());
} else {
System.out.println("Error: Brightness is out of range.");
}
}

28
 // Display max brightness
public static void option5(Light light) {
System.out.println("Max brightness is: " + light.getMaxBrightness());
}

// Display min brightness

public static void option6(Light light) {
System.out.println("Min brightness is: " + light.getMinBrightness());
}
}

Test Cases for Light

Test Cases Description Input Post Condition Expected Output

1 Display Light Status None Show the current light status Light is Currently
ON/OFF

2 Toggle Light Status Toggle the Light Stuatus toggled to ON in case of Light Status toggled.
status OFF or toggle to OFF in case of ON Now it is ON/OFF

3 Display Current Brightness None Show Current Brightness of the light Current Brightness
is:(value)

4 Set Brightnes within Range Any Integer System should set the brightness Brightness set to:
value according to user input (value)

5 Set Brightness outside range Any Integer System should show error message of Error: Brightness is
Value “Brightness is out of range” out of range

6 Display Max Brightness None System Should Diplay Max Brightness Max brightness is:
(value)

7 Display Min Brightness None System should display Min Brightness Min brightness is:
(value)

Test Case 1: Display Light Status

Result: Passed

Test Case 2: Toggle Light Status

Result: Passed

Test Case 3: Display Current Brightness

29
Result: Passed

Test Case 4: Set Brightness Within Range

Input Value: 50

Result: Passed

Test Case 5: Set Brightness outside range

Input value: 120

Result: Passed

Test Case 6: Display Max Brightness

Result: Passed

Test Case 7: Display Min Brightness

Result: Passed

2. Passive Infrared Sensor

Tester Class

import java.util.Scanner;
public class PassiveInfraredSensorTester {
public static void main(String[] args) {
Scanner scanner = new Scanner(System.in);
char choice;

try {
// Instantiate a new PassiveInfraredSensor object with initial parameters
PassiveInfraredSensor sensor = new PassiveInfraredSensor(101, 'A', 25);

do {
System.out.println("\n\t\tPassive Infrared Sensor Tester");
System.out.println("1. Detect person");
System.out.println("2. Quit");
System.out.print("Enter choice (1-2): ");

30
 choice = scanner.next().charAt(0);
System.out.println(); // blank line

switch (choice) {
case '1':
option1(sensor);
break;
case '2':
System.out.println("Exiting the tester.");
break;
default:
System.out.println("Invalid choice. Please enter a number between 1 and 2.");
}
} while (choice != '2');

} catch (Exception e) {
System.out.println("An error occurred: " + e.getMessage());
} finally {
scanner.close();
}
}

// Option to test detecting a person based on temperature

public static void option1(PassiveInfraredSensor sensor) {
Signal signal = sensor.detectPerson();
if (signal == Signal.PERSON_DETECTED) {
System.out.println("Person detected! Signal: " + signal);
} else {
System.out.println("No person detected. Signal: " + signal);
}
}

Test Description Input Expected Output Post Condition

Cases

1 Detecting a person with a Sensor ID: 101, "Person detected! Signal: Sensor should return
valid temperature range Room Name: "Room PERSON_DETECTED PERSON_DETECTED.
(between 20 and 40). A", Temperature: 25

2 No person detected when Sensor ID: 102, "No person detected. Sensor should return OFF.
the temperature is below Room Name: "Room Signal: OFF"
20. B", Temperature: 18

31
 3 No person detected when Sensor ID: 103, "No person detected. Sensor should return OFF.
the temperature is above Room Name: "Room Signal: OFF"
40. C", Temperature: 45

Test Case 1: Detecting a person with a valid temperature range (between 20 and 40).

Result: Passed

Test Case 2: No person detected when the temperature is below 20.

Result: Passed

Test Case 3: No person detected when the temperature is above 40.

Result: Passed

3. USER
Tester Class:
import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

public class SmartLightSystemTester {

public static void main(String[] args) {
char choice;
try {
// Setup test data
Map<String, Set<SmartLightSystem.Light>> roomLights = new HashMap<>();
32
 Set<SmartLightSystem.Light> lightsInICU = new HashSet<>();
lightsInICU.add(new SmartLightSystem.Light("ICU1"));
roomLights.put("ICU Room", lightsInICU);

SmartLightSystem.User user = new SmartLightSystem.User("ICU Room", 50, lightsInICU, roomLights);

do {
System.out.println("\n\t\tSmart Light System Tester\n");
System.out.println("1. Turn ON Light");
System.out.println("2. Turn OFF Light");
System.out.println("3. Set Brightness");
System.out.println("4. Scan Light QR Code");
System.out.println("5. Quit");
System.out.print("Enter choice 1-5: ");
choice = EasyIn.getChar(); // Accept a character entered at the keyboard

System.out.println(); // Blank line

try {
switch (choice) {
case '1':
option1(roomLights); // Turn ON light
break;
case '2':
option2(roomLights); // Turn OFF light
break;
case '3':
option3(user); // Set Brightness
break;
case '4':
option4(roomLights); // Scan QR Code for Light
break;
case '5':
System.out.println("Exiting the tester. Goodbye!");
break;
default:
System.out.println("Invalid choice. Please enter a number between 1 and 5.");
break;
}
} catch (IllegalArgumentException e) { // Handle illegal state or input
System.out.println("Error: " + e.getMessage());
}
} while (choice != '5');
} catch (IllegalArgumentException e) { // If initial setup breaks invariant

33
 System.out.println("Initial setup breaks invariant: " + e.getMessage());
EasyIn.pause("\nPress Enter to quit"); // Pause method of EasyIn
}
}

// Test method for turning on a light

public static void option1(Map<String, Set<SmartLightSystem.Light>> roomLights) {
System.out.print("Enter room name: ");
String roomName = EasyIn.getString();
System.out.print("Enter light ID to turn ON: ");
String lightId = EasyIn.getString();
String result = SmartLightSystem.turnOnLight(roomName, lightId, roomLights);
System.out.println("Result: " + result);
}

// Test method for turning off a light

public static void option2(Map<String, Set<SmartLightSystem.Light>> roomLights) {
System.out.print("Enter room name: ");
String roomName = EasyIn.getString();
System.out.print("Enter light ID to turn OFF: ");
String lightId = EasyIn.getString();
String result = SmartLightSystem.turnOffLight(roomName, lightId, roomLights);
System.out.println("Result: " + result);
}

// Test method for setting brightness

public static void option3(SmartLightSystem.User user) {
System.out.print("Enter new brightness (0-100): ");
int newBrightness = EasyIn.getInt();
String result;
try {
result = SmartLightSystem.setBrightness(user, newBrightness);
System.out.println("Brightness change result: " + result);
} catch (IllegalArgumentException e) {
System.out.println("Error: " + e.getMessage());
}
}

// Test method for scanning a light's QR code

public static void option4(Map<String, Set<SmartLightSystem.Light>> roomLights) {
System.out.print("Enter room name: ");
String roomName = EasyIn.getString();
System.out.print("Enter light ID to scan: ");
String lightId = EasyIn.getString();

34
 try {
SmartLightSystem.scanLightsQRCode(roomName, lightId, roomLights);
System.out.println("Light scanned and added successfully.");
} catch (IllegalArgumentException e) {
System.out.println("Error: " + e.getMessage());
}
}
}

TEST CASES FOR USER

Test Case
ID Description Input Precondition Expected Result Postcondition
Room name: Light with ID "ICU1" System turns on the The specified light in
Turn ON ICU Room, exists in "ICU Room" specified light and confirms the specified room is
TC-01 light Light ID: ICU1 and is currently OFF with a success message now ON
Turn ON Room name: Room exists but Error message indicating No change in the
non-existent ICU Room, specified light ID does the light does not exist in system; no new light
TC-02 light Light ID: ICU2 not the specified room is created
Room name: Light with ID "ICU1" System turns off the The specified light in
Turn OFF ICU Room, exists in "ICU Room" specified light and confirms the specified room is
TC-03 light Light ID: ICU1 and is currently ON with a success message now OFF
Turn OFF Room name: Room exists but Error message indicating No change in the
non-existent ICU Room, specified light ID does the light does not exist in system; no new light
TC-04 light Light ID: ICU2 not the specified room is created
Set
brightness User object is valid, System adjusts brightness to User's brightness
within New brightness brightness can be specified level and confirms level is updated to the
TC-05 range level: 75 adjusted with a success message specified value
Set User object is valid, but
brightness New brightness input is out of range (0- Error message indicating User's brightness
TC-06 out of range level: 150 100) invalid brightness range remains unchanged
Scan and Room name: Room exists, light ID System adds light to room The specified light ID
add light via ICU Room, does not exist, QR code and confirms with success is now added to the
TC-07 QR code Light ID: ICU2 scanning is supported message room
No changes are made
Scan non- Room name: to the system; no new
existent Unknown Room, Specified room does not Error message indicating room or light is
TC-08 room Light ID: ICU3 exist in the system the room does not exist created
Invalid Error message prompting No changes to the
menu Choice: '6' (any the user to enter a valid system; user
TC-09 choice invalid number) None choice prompted again

35
Test Case 1: Turn On Light
● Input: Room Name: ICU Room, Light ID: ICU1
● System Response: "Light ICU1 in ICU Room has been turned ON."
● Result: Passed

Test Case 2: Turn ON Non-Existent Light

● Input: Room Name: ICU Room, Light ID: ICU2
● System Response: "Error: Light ID ICU2 not found in ICU Room."
● Result: Passed

Test Case 3: Turn OFF Light

● Input: Room Name: ICU Room, Light ID: ICU1
● System Response: "Light ICU1 in ICU Room has been turned OFF."
● Result: Passed

Test Case 4: Turn OFF Non-Existent Light

● Input: Room Name: ICU Room, Light ID: ICU3
● System Response: "Error: Light ID ICU3 not found in ICU Room."
● Result: Passed

Test Case 5: Set Brightness Within Range

● Input Value: 75
● System Response: "Brightness successfully set to 75."
● Result: Passed

Test Case 6: Set Brightness Outside Range

● Input Value: 150
● System Response: "Error: Brightness level 150 is out of range (0-100)."
● Result: Passed

Test Case 7: Scan and Add Light via QR Code

● Input: Room Name: ICU Room, Light ID: ICU2
● System Response: "Light ICU2 has been successfully scanned and added to ICU Room."
● Result: Passed

Test Case 8: Scan Light in Non-Existent Room

● Input: Room Name: Unknown Room, Light ID: ICU3
● System Response: "Error: Room Unknown Room not found."
● Result: Passed

36
Test Case 9: Invalid Menu Choice
● Input: Choice: 6
● System Response: "Invalid choice. Please enter a number between 1 and 5."
● Result: Passed

4. LIGHT COONTROLLER
Tester Class
import java.util.Scanner;
import java.util.ArrayList;
import java.util.List;

public class LightControllerTester {

public static void main(String[] args) {
Scanner scanner = new Scanner(System.in);
LightController controller = new LightController();

List<Light> room1Lights = new ArrayList<>();

room1Lights.add(new Light("QR123", 1, 100, false));
room1Lights.add(new Light("QR124", 2, 100, false));
controller.roomLights.put("Room1", room1Lights);

List<Light> room2Lights = new ArrayList<>();

room2Lights.add(new Light("QR125", 3, 100, false));
controller.roomLights.put("Room2", room2Lights);

char choice;
do {
System.out.println("\n\t\tLight Controller Tester\n");
System.out.println("1. Display light status by ID");
System.out.println("2. Toggle light status by ID");
System.out.println("3. Display current brightness of a light");
System.out.println("4. Set brightness of a light");
System.out.println("5. Detect person in room (turn on all lights)");
System.out.println("6. Quit");
System.out.print("Enter choice (1 - 6): ");
choice = scanner.next().charAt(0);
System.out.println();

switch (choice) {
case '1':
displayLightStatus(controller, scanner);
break;
case '2':
toggleLightStatus(controller, scanner);
break;
case '3':
displayBrightness(controller, scanner);
break;
case '4':
setBrightness(controller, scanner);

37
 break;
case '5':
detectPerson(controller);
break;
case '6':
System.out.println("Exiting...");
break;
default:
System.out.println("Invalid choice. Please enter a number between 1 and 6.");
break;
}
} while (choice != '6');

scanner.close();
}

public static void displayLightStatus(LightController controller, Scanner scanner) {

System.out.print("Enter light ID: ");
while (!scanner.hasNextInt()) {
System.out.print("Please enter a valid integer for light ID: ");
scanner.next(); // consume invalid input
}
int lightId = scanner.nextInt();
boolean status = controller.getLightStatus(lightId);
System.out.println("Light with ID " + lightId + " is currently " + (status ? "ON" : "OFF"));
}

public static void toggleLightStatus(LightController controller, Scanner scanner) {

System.out.print("Enter room name: ");
String roomName = scanner.next(); // No change needed here
System.out.print("Enter light ID: ");
while (!scanner.hasNextInt()) {
System.out.print("Please enter a valid integer for light ID: ");
scanner.next(); // consume invalid input
}
int lightId = scanner.nextInt();
scanner.nextLine(); // Clear the newline
controller.setLightMode(lightId, roomName);
System.out.println("Light with ID " + lightId + " toggled.");
}

public static void displayBrightness(LightController controller, Scanner scanner) {

System.out.print("Enter room name: ");
String roomName = scanner.next();
System.out.print("Enter light ID: ");
while (!scanner.hasNextInt()) {
System.out.print("Please enter a valid integer for light ID: ");
scanner.next(); // consume invalid input
}
int lightId = scanner.nextInt();
scanner.nextLine(); // Clear the newline
List<Light> lights = controller.matchLight(lightId, roomName);

38
 if (lights != null && !lights.isEmpty()) {
System.out.println("Current brightness of light with ID " + lightId + " is: " + lights.get(0).brightness);
} else {
System.out.println("Light with ID " + lightId + " not found in " + roomName);
}
}

public static void setBrightness(LightController controller, Scanner scanner) {

System.out.print("Enter room name: ");
String roomName = scanner.next();
System.out.print("Enter light ID: ");
while (!scanner.hasNextInt()) {
System.out.print("Please enter a valid integer for light ID: ");
scanner.next(); // consume invalid input
}
int lightId = scanner.nextInt();
System.out.print("Enter brightness level (0 - 100): ");
while (!scanner.hasNextInt()) {
System.out.print("Please enter a valid integer for brightness level: ");
scanner.next(); // consume invalid input
}
int brightness = scanner.nextInt();
scanner.nextLine(); // Clear the newline
controller.setBrightness(roomName, lightId, brightness);
System.out.println("Brightness of light with ID " + lightId + " set to: " + brightness);
}

public static void detectPerson(LightController controller) {

controller.personDetection(true);
System.out.println("Person detected. All lights in every room turned ON.");
}
}

TEST CASES FOR LIGHT CONTROLLER

Test Description Input Precondition Expected Result Postcondition
Case ID

TC001 Display light lightId Light with ID exists in System displays Light status
status by ID a room and has a set whether the light is displayed
status ON or OFF accurately

TC002 Toggle light roomName, lightId Light with ID exists Light status toggles Light status toggled
status by ID and is either ON or (ON to OFF or OFF and reflected in the
OFF to ON) system

TC003 Set brightness roomName, Light with ID exists Brightness of the Brightness level is
of a light lightId,brightness and is OFF or ON light is set to the updated to the
entered value specified level

39
 TC004 Detect person _ One or more lights are All lights in each Lights are turned
in room OFF in each room room are turned ON ON in all rooms
upon detection

Test Case 1: Display Light Status by ID

Result: PASS

Test Case 2: Toggle Light Status by ID (Turning Light On)

Result: PASS (Light status changes from OFF to ON)

Test Case 3: Set Brightness of a Light (Enter brightness level (0 -100): 75)

Result: PASS (Brightness changes successfully to 75)

Test Case 4: Detect Person (Turn on All Lights in All Rooms)

Result: PASS (All lights should now be ON)

Test Case 5: Exit Program

40
LESSONS LEARNED AND CHALLENGES FACED

● Ensuring Consistency Across Architectural Views and Specifications: One of the main challenges was
keeping the 4+1 architectural views, VDM-SL specification, and Java code aligned, especially as design changes
occurred during development. Regular cross-referencing between views and specifications proved essential, as it
ensured that any updates were reflected throughout the documentation.
● Lesson Learned: Incremental review and synchronization of all views, specs, and code significantly improve the
coherence and maintainability of complex documentation.

● Implementing Pre- and Post-Conditions to Guarantee Code Robustness: Defining and integrating pre- and
post-conditions in Java required careful planning to capture edge cases without complicating the code flow. We
found that testing each condition individually not only helped catch subtle issues but also improved the overall
reliability of the system.
● Lesson Learned: Testing conditions in isolation and keeping them modular allowed for more targeted debugging
and validation, enhancing code quality and readability.

● Balancing Technical Detail with Readability in the Report: It was challenging to include detailed
specifications, code snippets, and architecture justifications without overwhelming the reader. Breaking down
sections into manageable parts and adding summaries allowed the report to remain comprehensive yet
approachable.
● Lesson Learned: Providing clear summaries and using visual aids like diagrams made technical content more
accessible, which is essential for ensuring understanding among a broader audience.

41