Commit c5346850 authored by Lars Hermerschmidt's avatar Lars Hermerschmidt

Adding evaluation models

parent 8e853a93
package secarc.supermarket;
import secarc.supermarket.msg.*;
import secarc.supermarket.imp.CashDesk;
import secarc.supermarket.imp.WebSite;
component Supermarket {
trustlevel +0;
accesscontrol off;
// cash desk ports
port
in Event newSale,
in Image barcode,
out ProductData outPDataNS,
in Event endSale;
port
in Event payCash,
in Double amountMoney,
out Double outAmountChange;
port
in Event payCard,
in CardData cardDataPC,
in Integer pinPC,
out Boolean outValidationPC;
port
in Event payOnline,
in AccountData accDataPO,
in Integer pinPO,
out Boolean outValidationPO;
port
in Event getCash,
in CardData cDataGC,
in Integer pinGC,
out Double outAmountMoney;
component CashDesk cashDesk;
connect newSale -> cashDesk.newSale;
connect barcode -> cashDesk.barcode;
connect cashDesk.outPDataNS -> outPDataNS;
connect endSale -> cashDesk.endSale;
connect payCash -> cashDesk.payCash;
connect amountMoney -> cashDesk.amountMoney;
connect cashDesk.outAmountChange -> outAmountChange;
connect payCard -> cashDesk.payCard;
connect cardDataPC -> cashDesk.cardDataPC;
connect pinPC -> cashDesk.pinPC;
connect cashDesk.outValidationPC -> outValidationPC;
connect payOnline -> cashDesk.payOnline;
connect accDataPO -> cashDesk.accDataPO;
connect pinPO -> cashDesk.pinPO;
connect cashDesk.outValidationPO -> outValidationPO;
connect getCash -> cashDesk.getCash;
connect cDataGC -> cashDesk.cDataGC;
connect pinGC -> cashDesk.pinGC;
connect cashDesk.outAmountMoney -> outAmountMoney;
// web service ports
port
in Event newOrder,
in Integer productId,
out ProductData outPDataNO,
in Event endOrder;
port
in Event payOnlineWeb,
in AccountData accDataPOW,
in Integer pinPOW,
out Boolean outValidationPOW;
component WebSite webSite;
connect newOrder -> webSite.newOrder;
connect productId -> webSite.productId;
connect webSite.outPDataNO -> outPDataNO;
connect endOrder -> webSite.endOrder;
connect payOnlineWeb -> webSite.payOnlineWeb;
connect accDataPOW -> webSite.accDataPOW;
connect pinPOW -> webSite.pinPOW;
connect webSite.outValidationPOW -> outValidationPOW;
}
package secarc.supermarket.imp;
import secarc.supermarket.msg.*;
component Accounting{
// data center ports
trustlevel +1;
accesscontrol on;
access employeeAccount;
port
out Request outRequestInfo,
in StockInfo stockInfo,
out Update outUpdateStockInfo;
// warehouse ports
port
out Request outRequestGoods,
in Boolean acknowledge,
in Boolean deliveryAck;
component Warehouse warehouse;
// accounting -> warehouse
connect outRequestGoods -> warehouse.requestGoods;
connect warehouse.outAcknowledge -> acknowledge;
connect warehouse.outDeliveryAck -> deliveryAck;
}
package secarc.supermarket.imp;
import secarc.supermarket.msg.*;
component Bank{
accesscontrol on;
trustlevel +2;
access accountData(customer);
access transactionInfo(customer);
// cash desk ports
port
in AccountData accountDataCD,
in TransactionInfo transactionInfoCD,
out Boolean outAcknowledgeCD;
// web site ports
port
in AccountData accountDataWS,
in TransactionInfo transactionInfoWS,
out Boolean outAcknowledgeWS;
}
package secarc.supermarket.imp;
import secarc.supermarket.msg.*;
component CashDesk{
accesscontrol off;
trustlevel +0;
// super market ports
port
in Event newSale,
in Image barcode,
out ProductData outPDataNS,
in Event endSale;
port
in Event payCash,
in Double amountMoney,
out Double outAmountChange;
port
in Event payCard,
in CardData cardDataPC,
in Integer pinPC,
out Boolean outValidationPC;
port
in Event payOnline,
in AccountData accDataPO,
in Integer pinPO,
out Boolean outValidationPO;
port
in Event getCash,
in CardData cDataGC,
in Integer pinGC,
out Double outAmountMoney;
// data center ports
port
out Integer outProductId,
in ProductData productData,
out SaleInfo outSaleInfo;
// bank ports
port
out AccountData outAccountData,
out TransactionInfo outTransactionInfo,
in Boolean acknowledge;
component DataCenter dataCenter;
component Bank bank;
// cashDesk -> dataCenter
connect outProductId -> dataCenter.productIdCD;
connect dataCenter.outProductDataCD -> productData;
connect outSaleInfo -> dataCenter.saleInfo;
// cashDesk -> bank
connect encrypted outAccountData -> bank.accountDataCD;
connect encrypted outTransactionInfo -> bank.transactionInfoCD;
connect bank.outAcknowledgeCD -> acknowledge;
}
package secarc.supermarket.imp;
import secarc.supermarket.msg.*;
component DataCenter{
accesscontrol on;
trustlevel +2;
access employeeIT;
// web site ports
port
in Integer productIdWS,
out ProductData outProductDataWS,
in OrderInfo orderInfo;
// cash desk ports
port
in Integer productIdCD,
out ProductData outProductDataCD,
in SaleInfo saleInfo;
// accounting ports
port
in Request requestInfo,
out StockInfo outStockInfo,
in Update updateStockInfo;
component WebServer webServer{
autoconnect port;
// web service ports
port
in Integer productIdWS,
out ProductData outProductDataWS,
in OrderInfo orderInfo;
}
component WebSite webSite;
component Accounting accounting;
// dataCenter -> webSite
connect webSite.outProductId -> productIdWS;
connect outProductDataWS -> webSite.productData;
connect webSite.outOrderInfo -> orderInfo;
// dataCenter -> accounting
connect accounting.outRequestInfo -> requestInfo;
connect outStockInfo -> accounting.stockInfo;
connect accounting.outUpdateStockInfo -> updateStockInfo;
}
package secarc.supermarket.imp;
import secarc.supermarket.msg.*;
component Warehouse{
accesscontrol on;
trustlevel +1;
access employeeWarehouse;
// accounting ports
port
in Request requestGoods,
out Boolean outAcknowledge,
out Boolean outDeliveryAck;
}
\ No newline at end of file
package secarc.supermarket.imp;
import secarc.supermarket.msg.*;
component WebSite{
accesscontrol off;
trustlevel +0;
// super market ports
port
in Event newOrder,
in Integer productId,
out ProductData outPDataNO,
in Event endOrder;
port
in Event payOnlineWeb,
in AccountData accDataPOW,
in Integer pinPOW,
out Boolean outValidationPOW;
// data center.web server ports
port
out Integer outProductId,
in ProductData productData,
out OrderInfo outOrderInfo;
// bank ports
port
out AccountData outAccountData,
out TransactionInfo outTransactionInfo,
in Boolean acknowledge;
component Bank bank;
// webSite -> bank
connect outAccountData -> bank.accountDataWS;
connect outTransactionInfo -> bank.transactionInfoWS;
connect bank.outAcknowledgeWS -> acknowledge;
}
This diff is collapsed.
package msg;
public class AccountData {
}
\ No newline at end of file
package msg;
public class CardData {
}
\ No newline at end of file
package msg;
public class Event {
}
\ No newline at end of file
package msg;
public class Image {
}
\ No newline at end of file
package msg;
public class OrderInfo {
}
\ No newline at end of file
package msg;
public class ProductData {
}
\ No newline at end of file
package msg;
public class Request {
}
\ No newline at end of file
package msg;
public class SaleInfo {
}
\ No newline at end of file
package msg;
public class StockInfo {
}
\ No newline at end of file
package msg;
public class TransactionInfo {
}
\ No newline at end of file
package msg;
public class Update {
}
\ No newline at end of file
package secarc.seccds;
// import message types
import secarc.seccds.msg.*;
import java.awt.Image;
// import components
import secarc.seccds.fe.Supermarket;
import secarc.seccds.fe.Rack;
import secarc.seccds.fe.SelfServiceCashDesk;
import secarc.seccds.be.Bank;
import secarc.seccds.de.OnlineStore;
import secarc.seccds.de.QuickCashDesk;
import secarc.seccds.ae.AccountingDepartment;
import secarc.seccds.hr.HighRackWarehouse;
import secarc.seccds.ke.DataCenter;
import secarc.seccds.ke.Webserver;
component SuperMarketTradingSystem {
identity weak onlineStore -> dataCenter.webServer;
identity weak dataCenter.webServer -> accountingDepartment;
autoconnect encrypted port;
autoinstantiate on;
accesscontrol off;
port
in Event newPreOrder,
in Image product,
in Event endPreOrder,
in Event confirmPreOrd,
in Boolean confirmation,
in AccountLogin,
in Boolean reply,
in OnlineLogin,
out ProductData outPData,
out Event offerOnlinePay,
out Event onlinePay,
out Boolean validation;
component Bank;
component Supermarket;
component HighRackWarehouse;
component AccountingDepartment;
component DataCenter;
}
package secarc.seccds.be;
// import message types
import secarc.seccds.msg.*;
component AccountingDepartment {
identity weak accountingDepartment -> dataCenter.webServer;
port
in RealTimeStockInformation;
}
package secarc.seccds.be;
// import message types
import secarc.seccds.msg.*;
component Bank {
trustlevel +3;
port
critical in BankData,
critical in OnlineBankData,
out CashOut,
out PaymentAck;
access bankData (customer);
access onlineBankData (customer);
}
package secarc.seccds.be;
// import message types
import secarc.seccds.msg.*;
import secarc.seecds.de.QuickCashDesk;
component OnlineStore {
trustlevelrelation onlineStore < quickCashDesk;
trustlevelrelation quickCashDesk < bank;
identity strong quickCashDesk -> bank;
port
in Event newPreOrder,
in Image product,
out ProductData outPData,
in Event endPreOrder,
in Event confirmPreOrd,
critical in AccountLogin,
in Boolean confirmation,
out Event offerOnlinePay,
in Boolean reply,
out Event onlinePay;
port
out String identifier,
in ProductData inPData;
port
in checkPayment,
out PaymentAck;
component QuickCashDesk quickCashDesk
[encrypted onlineBdOut -> bank.onlineBdData;];
connect dataCenter.webServer.outPData -> onlineStore.inPData;
connect encrypted bank.paymentAck -> onlineStore.quickCashDesk.opIn;
}
package secarc.seccds.be;
// import message types
import secarc.seccds.msg.*;
component QuickCashDesk {
trustlevelrelation quickCashDesk < bank;
trustlevelrelation quickCashDesk < onlineStore;
port
critical in OnlineLogin,
critical out OnlineBankData onlineBdOut,
in PaymentAck opIn,
out Boolean validation;
}
package secarc.seccds.fe;
// import message types
import secarc.seccds.msg.*;
component Rack {
accesscontrol on;
autoconnect port;
access customer, workers, deliveryMen;