Before the lab classes: prepare HML file, which contains a complete ARD model of the system designed in the previous lab classes.
./hqed
/home/users/students/ins5/esimon/hqed/hqed
Having a complete ARD model of a system, the next step is to generate a XTT preliminary model. It can be done by:
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.
Name | Base | Domain | Scale | Ordered | Desc |
---|---|---|---|---|---|
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 |
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.
Name | Multiplicity | Type | Relation | Callback | Acronym | Description |
---|---|---|---|---|---|---|
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 |
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:
(?)enteredPin | (?)correctPin | (→)pinDifference |
---|
=any | =any | :=sub(correctPin, entered(Pin) |
(?)pinDifference | (→)authorizated | (→)failedAttempts |
---|
!=0 | :=false | :=add(failedAttempts,1) |
=0 | :=true | :=failedAttempts |
(?)desiredAmount | (?)userAccountAmount | (→)udAmountDifference |
---|
=any | =any | :=sub(userAccountAmount, desiredAmount) |
(?)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.
The HQEd tool allows for defining of initial states in the States panel.
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:
label
.Z braku lepszego miejsca tutaj studenci wpisują komentarze natury ogólnej do tego lab.
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:)