nz.ac.waikato.modeljunit.examples.gsm
Class SimCard

java.lang.Object
  nz.ac.waikato.modeljunit.examples.gsm.SimCard

All Implemented Interfaces:

FsmModel

public class SimCard
extends java.lang.Object
implements FsmModel

This is an EFSM model of the SIM card within a mobile phone. It models just a small part of the functionality to do with accessing files and directories within the SIM card, and the PINs and PUKs used to make this secure. See Chapter 11 of the book "Practical Model-Based Testing: A Tools Approach" for more discussion of this system and a version of the model in B. This ModelJUnit version of the model was translated from a UML/OCL model developed at LEIRIOS Technologies, which in turn was adapted from an earlier and larger version of the B model published in the above book.

Author:

marku

Nested Class Summary

static class	SimCard.B_Status
static class	SimCard.E_Status
static class	SimCard.F_Name
static class	SimCard.File_Type
static class	SimCard.Permission
static class	SimCard.Status_Word

Field Summary

protected int	counter_PIN_try
protected int	counter_PUK_try
protected File	DF
protected File	EF
protected java.util.Map<SimCard.F_Name,File>	files
static int	Max_Pin_Try
static int	Max_Puk_Try
protected boolean	perm_session
protected int	PIN
protected static int	PUK
protected java.lang.String	read_data
protected SimCard.Status_Word	result
protected SimCard.B_Status	status_block
protected SimCard.E_Status	status_en
protected SimCard.B_Status	status_PIN_block
protected SimCardAdaptor	sut If this is non-null, each action calls the corresponding adaptor action, which tests the GSM11 implementation.

Constructor Summary

SimCard(SimCardAdaptor sut0)
If sut0 is null, then the model runs without testing any SUT.

Method Summary

void	Change_PIN(int old_Pin, int new_Pin)
void	changePinNew()
void	changePinSame()
void	Disabled_PIN(int Pin)
void	disablePINGood()
void	Enabled_PIN(int Pin)
void	enablePIN11()
java.lang.Object	getState() Return the current state of the FSM model.
static void	main(java.lang.String[] args)
void	Read_Binary()
void	reset(boolean testing) Reset the model to its initial state.
void	Select_file(SimCard.F_Name file_name)
void	selectDF_Gsm()
void	selectDF_Roaming()
void	selectEF_FR()
void	selectEF_IMSI()
void	selectEF_LP()
void	selectMF()
void	Unblock_PIN(int Puk, int new_Pin)
void	unblockPINBad()
void	unblockPINGood12()
void	Verify_PIN(int Pin)
void	verifyPIN11()
void	verifyPIN12()

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, toString, wait, wait, wait

Field Detail

PIN

protected int PIN

PUK

protected static final int PUK

See Also:

Constant Field Values

status_en

protected SimCard.E_Status status_en

status_PIN_block

protected SimCard.B_Status status_PIN_block

status_block

protected SimCard.B_Status status_block

counter_PIN_try

protected int counter_PIN_try

counter_PUK_try

protected int counter_PUK_try

perm_session

protected boolean perm_session

Max_Pin_Try

public static final int Max_Pin_Try

See Also:

Constant Field Values

Max_Puk_Try

public static final int Max_Puk_Try

See Also:

Constant Field Values

read_data

protected java.lang.String read_data

result

protected SimCard.Status_Word result

DF

protected File DF

EF

protected File EF

files

protected java.util.Map<SimCard.F_Name,File> files

sut

protected SimCardAdaptor sut

If this is non-null, each action calls the corresponding adaptor action, which tests the GSM11 implementation.

Constructor Detail

SimCard

public SimCard(SimCardAdaptor sut0)

If sut0 is null, then the model runs without testing any SUT.

Parameters:

sut0 - Can be null.

Method Detail

getState

public java.lang.Object getState()

Description copied from interface: FsmModel

Return the current state of the FSM model. The objects returned by this method define the states (the nodes) of the finite state machine. The objects that are returned must have a correct implementation of the equals method, since this is used to decide whether two states are the same or not. It is common to return a string, but other kinds of objects can be used if desired (in which case, their toString() method will be used to get a printable form of each FSM state).

Advanced Feature: This method can be used to define equivalence classes over the states, if you want to reduce the number of states to keep the FSM small. For example, if you have a integer state variable I that can have a huge number of possible values, you could define your getState() method to return new Integer(I % 10). This would reduce the FSM to just 10 states, where FSM state 0 represents all the states where I=0 or I=10 or I=20 etc., and FSM state 1 represents all the states where I=1 or I=11 or I=21 etc.

Specified by:

getState in interface FsmModel

Returns:

An object that represents the current state.

reset

public void reset(boolean testing)

Description copied from interface: FsmModel

Reset the model to its initial state. If the testing parameter is true, then this reset and all the following actions should affect the SUT.

Specified by:

reset in interface FsmModel

Parameters:

testing - true means the SUT should be reset too.

verifyPIN11

public void verifyPIN11()

verifyPIN12

public void verifyPIN12()

Verify_PIN

public void Verify_PIN(int Pin)

unblockPINGood12

public void unblockPINGood12()

unblockPINBad

public void unblockPINBad()

Unblock_PIN

public void Unblock_PIN(int Puk,
                        int new_Pin)

enablePIN11

public void enablePIN11()

Enabled_PIN

public void Enabled_PIN(int Pin)

disablePINGood

public void disablePINGood()

Disabled_PIN

public void Disabled_PIN(int Pin)

changePinSame

public void changePinSame()

changePinNew

public void changePinNew()

Change_PIN

public void Change_PIN(int old_Pin,
                       int new_Pin)

selectMF

public void selectMF()

selectDF_Gsm

public void selectDF_Gsm()

selectDF_Roaming

public void selectDF_Roaming()

selectEF_IMSI

public void selectEF_IMSI()

selectEF_LP

public void selectEF_LP()

selectEF_FR

public void selectEF_FR()

Select_file

public void Select_file(SimCard.F_Name file_name)

Read_Binary

public void Read_Binary()

main

public static void main(java.lang.String[] args)
                 throws java.io.FileNotFoundException

Throws:

java.io.FileNotFoundException