print · login   


Tag: register

Related publications: [AHKOV12]


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  


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.


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