print · source · login   

Login

Related publications: [AHKOV12]

Description

Figure 1 depicts a Mealy machine that describes a simple login procedure. A user may register to the system by choosing a login name and password. Then the user may login to the system using the values selected during the registration. When being logged in, the user may log out. The user is never allowed to change his login credentials.

Mealy machine model of a login system
Fig. 2: Mealy machine model of a login system  

The SUT

We used the Uppaal [BDL04] GUI as an editor to create an extended finite state machine (EFSM) of the Login system. By means of several Python scripts we automatically generated from the Uppaal .xml file a Java executable that represents the EFSM as a Java state machine and acts as SUT.

Resources

model.pdf Δ   7Kb   February 14, 2015, at 07:44 PM
model.register.xml Δ   3Kb   February 14, 2015, at 07:44 PM
model.svgz Δ   3Kb   February 20, 2015, at 03:49 AM
model.uppaal.xml Δ   4Kb   February 14, 2015, at 07:44 PM