Spis treści

Expert System Design

Preparation

Before the lab classes: prepare HML file, which contains a complete ARD model of the system designed in the previous lab classes.

XTT Design

HQed

Creating XTT preliminary model

Having a complete ARD model of a system, the next step is to generate a XTT preliminary model. It can be done by:

Types defining

The types defining is a one of the most important steps during the design. The automatically generated model has defined only a one type named default, which is related with all attributes. The appropriate definition of the types allows for full exploiting of the Hekate advantages from the formal verification point of view.

NameBaseDomainScaleOrderedDesc
tPin numeric [0; 9999] 0 yes Represents the PIN numbers
tPinDifferene numeric [-9999; 9999] 0 yes Represents all the possible results of two PIN numbers subtraction
tUserActions symbolic {withdraw; balance} - no The set of actions that user can invoke
tCashPointActivities symbolic {askForPIN; payOut; takeCardAway; displayBalance;
msgNotEnoughFoundsInMachine; msgNotEnoughFoundsOnAccount;}
- no The set of actions that can be executed by cashpoint
tMoney numeric no constraints 2 yes Represents the amount of money
tBool symbolic {false, true} 0 yes The boolean values
tAttempts numeric [0; 3] 0 yes The type that defines the number of attempts to enter a correct PIN

Attributes defining

The complete ARD model should contain all the attributes, which describe the system, and dependencies between them. However, it does not contain any information about types. This is due to the fact, that neither of tools VARDA nor HJEd do not support types defining. Thus, the next step is to define attributes type and the other properities.
The following table contains all the attributes that should be defiend. The last column contains an optional attribute description.

NameMultiplicityTypeRelationCallbackAcronymDescription
userRequestedAction simple tUserActions input - userR Indicates the action that user wants to execute
cashPointActivity simple tCashPointActivities output - cashP Indicates which action should be invoked by cashpoint
correctPin simple tPin input - corre Holds the PIN number that is stored on the card
enteredPin simple tPin input - enter Holds the PIN number that has been entered by the user
pinDifference simple tPin input/output - pinDi Holds the difference between enteredPin attribute value and correctPin attribute value
authorized simple tBool input/output - autho Indicates if the user has entered a correct PIN
failedAttempts simple tAttempts input/output - faile Holds the number of failed attemts to the entering of a PIN
desiredAmount simple tMoney input - desir Holds the amount of money, which user wants to withdraw
cashPointAmount simple tMoney input - cash The amount of money inside cashpoint
userAccountAmount simple tMoney input - userA The total balance of the user account
cdAmountDifference simple tMoney input/output - cdAmo Holds the difference between cashPointAmount attribute value and desiredAmount attribute value
udAmountDifference simple tMoney input/output - udAmo Holds the difference between userAccountAmount attribute value and desiredAmount attribute value

Rules defining

Definiowanie reguł jest najważniejszym elementem tej fazy projektowania. Otrzymany na bazie modelu ARD diagram XTT zawiera tylko nagłówki tabel, które winny zostać wypełnione regułami oraz uzupełnione o odpowiednie połączenia. Poniżej znajduje się lista reguł, które należy zdefiniować w modelu XTT systemu bankomat. W poniższych regułach przejęto nazwy atrybutów z poprzedniego ćwiczenia.

Rules defining is the most important stage of the design. The ARD model provides only the schemas (headers) of the XTT tables, which must be filled with rules. Below the list of all rules, which must be defined, can be found:

Table 1

(?)enteredPin(?)correctPin (→)pinDifference
=any =any :=sub(correctPin, entered(Pin)

Table 2

(?)pinDifference (→)authorizated(→)failedAttempts
!=0 :=false :=add(failedAttempts,1)
=0 :=true :=failedAttempts

Table 3 and 4

(?)desiredAmount(?)userAccountAmount (→)udAmountDifference
=any =any :=sub(userAccountAmount, desiredAmount)

Table 5

(?)authorizated(?)failedAttempts(?)userRequestedAction(?)udAmountDifference(?)cdAmountDifference (→)cashPointActivity
=false <3 =any =any =any :=askForPIN
=false =3 =any =any =any :=takeCardAway
=true =any =balance =any =any :=displayBalance
=true =any =withdraw >=0 >=0 :=payOut
=true =any =withdraw =any <0 :=msgNotEnoughFoundsInMachine
=true =any =withdraw <0 >=0 :=msgNotEnoughFoundsOnAccount

After the rules design stage, the model must be complemented by defining the connections between tables. Usually, all the rules in the given table are connected to the same table. The connection of the first rule is determined by ARD→XTT transition algorithm.

Initial states defining

The HQEd tool allows for defining of initial states in the States panel.

Model testing

Before the physical implementation, the simulation of the system can be performed. The simulation can be executed by built-in engine or with the help of external plugin. During the calsses at least one type of simulation should be done for at least two different initial states.
The simulation can be performed by:

HMR

Comments

Z braku lepszego miejsca tutaj studenci wpisują komentarze natury ogólnej do tego lab. 8-)

Definiowanie reguł nie ma szczegolowej instrukcji jak to ustawic Program sie zawieszaa:) nie ma w instrukcji zeby zapisac, a program sie zawiesza. Po restarcie brakuje tabel na dane wejsciowe Zamiast wpisywac recznie wszystkie typy, ciekawiej byloby to udostepnic do importu a moze w zamian pokazac 2-3 reguly i kazac jakas jedna samemu wymyslec?

naglowek Definiowanie atrybutów i Definiowanie typow sa zamienione:)