print · login   

Login

Tag: register

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 Δ   7K   February 14, 2015, at 07:44 PM
model.register.xml Δ   3K   February 14, 2015, at 07:44 PM
model.svgz Δ   3K   February 20, 2015, at 03:49 AM
model.uppaal.xml Δ   4K   February 14, 2015, at 07:44 PM