SE-2832 Introduction to Software Verification

Dr. Mark Sebern -- Spring quarter 2013-2014

Lab 7

Revised: 23 April 2014


This lab was developed by Dr. Walt Schilling; all errors in its adaptation are the responsibility of the instructor.


In this lab, you will work in a small team (2-3 members) to implement tests based on a state-machine specification. You may not do this lab by yourself.

Background information

The system you are to verify represents a security light. The security light has a light sensor which detects if it is night or day. During the day, the motion sensor is not active and the light will not turn on. However, at night, the system will look for motion, and if motion is found, the lamp will be turned on for 30 seconds. If at night the security alarm is tripped, the light will flash on and off until it is cleared by the user. The system also has a manual override switch which will turn the lamp on at any time.

A UI for this program has been developed for prototyping purposes, as is shown in the figure below. It allows the user to simulate inputs and monitor the behavior.


Formally, the behavior for this system is specified using the following UML state chart.
Note specifically the entry and exit actions for each of the states.


You can download the light controller source code from:

Lab Assignment

Using JUnit / TestNG and the jMock mock object tool, and the behavioral specification from the state machine, you are to develop a set of test cases to verify that the LightControllerStateMachine functions properly. (Hint: You may want to draw sequence diagrams from the state chart to determine the correct interactions and message sequences between objects.)

Once you have created the test cases, you are to verify the behavior of the LightControllerStateMachine. This involves running your tests on the program and correcting any problems you encounter. If there are any defects, fix them in the source code.

Assignment submission (due by 11:59PM CDT, Tuesday, April 29)

Prepare a PDF report (named "SE2832-username1-username2-username3-Lab7.pdf" (using dashes, not underscores, with the specified capitalization), where each "usernameN" is the lowercase MSOE email username of a team member) on your lab experience, including:

If you have any questions, consult the instructor.