The goal of this assignment is to familiarize yourself with Statechart modeling, simulation, debugging and, to a lesser extent, automatically checking requirements -specified as temporal logic formulas over behaviour traces- on your solution.
We will use the brand-new Statechart editor, simulation and testing environment StateBuddy, created by yours truly.
No need to install anything. StateBuddy runs in the browser.
Before we start working on this assignment, we will solve 5 small exercises. Each exercise shows you a small Statechart model, and asks a question about its behavior. If you can solve the exercises, you will have a good (enough) understanding of the precise semantics of StateBuddy.
The exercises can be opened by clicking on their respective links:
Example:
Consider the linked Statechart.
After initialization, the current states are: OrthogonalState, A, C, E.
Then, the Statechart remains idle until it receives an input event. Suppose at time T=5s, the input event e is received. This triggers the execution of an RTC step.
The RTC step starts with a fair-step, where regions r1, r2 and r3 (in that order) are allowed to fire at most one transition each.
Only r1 has an enabled transition (because event e is active), so only r1 fires.
During the firing of that transition, the internal event f is raised, an appended to the internal event queue.
The fair-step ends, and one more fair-step is executed, because the internal event queue is not empty.
So again, r1, r2 and r3 are allowed to fire at most one transition.
This time, the regions r2 and r3 will fire, because event f is active.
The second fair-step ends, and since the internal event queue is empty, the RTC step also ends.
Even though all transitions fired in a certain order, all of it happened at the same point in (simulated) time.
Now, the Statechart will again remain idle until another input event occurs.
Time r1 r2 r3 =0 Initialization enter A enter C enter E >0 && <5s Idle =5s RTC step (input=e) Fair-step (event=e) fire (exit A, raise f, enter B) Fair-step (event=f) fire (exit C, enter D) fire (exit E, enter F) =5s End of RTC step
You will use the Statecharts formalism to model the controller of a classic digital watch (before smart watches existed).
All user input happens through 4 buttons (one in each corner).
The watch can display 6 numbers, in the form HH:MM:SS when displaying the current time, or the time of the alarm, or in the form MM:SS:HS (HS means hectoseconds) when displaying the chronometer.
The watch has a background light that can be on or off.
The watch can make a beep-sound.
The time can be edited.
An alarm can be turned on or off. The alarm time can also be edited.
The chronometer can be started, paused, and reset.
You will implement the plant (= digital watch) controller as a Statechart. The controller only talks to the plant via input-events and output-events. In StateBuddy, you can also interactively raise input events directly into the controller statechart (Debugger UI). Finally, the plant also has its own UI, which sends input events to the plant.
For the curious student: Yes, the (simulated) plant is also implemented as a (rather big) Statechart.
| Controller input event(s) | Received when... |
|---|---|
| topLeftPressed, topRightPressed, bottomLeftPressed, bottomRightPressed | one of the 4 buttons is pressed |
| topLeftReleased, topRightReleased, bottomLeftReleased, bottomRightReleased | one of the 4 buttons is released |
| alarm | the alarm should go off |
| Controller output event(s) | Effect |
|---|---|
| lightOn, lightOff | turns on / off the background light |
| beep | make a beep sound for 10ms |
| incTime | increment the watch's time by one second |
| incChrono | increment the watch's chrono by 1/100 second |
| resetChrono | sets the chronometer back to 00:00:00 |
| displayTime | puts the watch into a mode where it displays the current time |
| displayChrono | puts the watch into a mode where it displays the chronometer |
| displayAlarm | puts the watch into a mode where it displays the time of the alarm |
| setAlarm(boolean) | turns the alarm on (true) or off (false). if the alarm is on, and the plant detects that the current time is equal to the alarm time, then the plant will immediately send the 'alarm' event (explained above) to the controller. |
| beginEdit | puts the plant into 'edit mode'. if the plant was displaying the current time, you can now edit the current time. if the plant was dispalying the alarm time, then you can now edit the alarm time. After entering edit mode, the 'hours' part of the display will start blinking, indicating that the 'hours' can be edited. |
| endEdit | ends the 'edit mode'. |
| incSelection | when in 'edit mode', will increase the currently blinking part (i.e, hours, minutes or seconds) of the display by one |
| selectNext | when in 'edit mode', will select the next item (hours -> minutes -> seconds -> hours) to edit |
Use this link to the starting point for this assignment.
To test your solution, initialize the execution, and interact with the plant UI. The execution can run in (scaled) real-time, with the ability to pause/resume.
To gain more confidence that you correctly implemented the requirements, you can write Metric Temporal Logic (MTL) properties. An example of such a property is:
G ((topRightPressed & (X ~topRightPressed)) -> (G[0,2000] (lightOn)))meaning: "as long as the top-right button is pressed, the light should be on, and after the top-right button is released, the light should remain on for 2 seconds" AKA Requirement 1.
Note that none of these testing approaches are exhaustive (unlike model checking, which is exhaustive). Any property you write will only be checked on the current simulation trace.
You are also required to write a small(*) (HTML or PDF) report.
(*) I don't have time to read 100 pages!
It must include the following:
Your solution needs to be precisely correct: superficially correct behavior when running the generated code with the GUI (e.g., seeing the water levels change) is not enough: the timing-related requirements are exact.
The assignment has been designed specifically to encourage use of as many Statechart features as possible:
Make sure you understand these features, and use them, where you think they are appropriate.
To give you an indication of the complexity, my own solution consists of 19 AND-states, 10 OR-states, and 36 transitions.