Ha Mai

Ask the question before create a static method X in java:

"Does it make sense if call X without any object has been constructed yet?"

See detail answer here:

1- download jre desired version here:

http://www.oracle.com/technetwork/java/archive-139210.html 

(accept the licence and download it)

2- run exe file to install jre.

Sometimes it’s neccessary to configure jre environment on window:

Right click Computer-> Properties-> Advanced system settings-> Environment variables.

System variables-> New

Fill information:

Variable name: JAVA_HOME

Variable value: the directory where jre is stored (e.g. C:\Program Files\Java\jre7)

3- configure jre in eclipse:

Window -> Preferences-> java-> Install JREs.

Then click Add->Standard VM -> JRE Home.

Point to the directory where jre is stored (e.g. C:\Program Files\Java\jre7)

Critical system: Failure can result in significant economic losses, physical damage or threats to ge or threats to human life.

Safety--critical systems Failure results in loss of life, injury or damage to the environment ment Chemical plant protection system

Mission--critical systems Failure results in failure of some goal Failure results in failure of some goal--directed activity Spacecraft navigation system

The current solution:

Static Access Control --> SecureUML

Dynamic properties --> Activity diagram

Transformation into B method

SecureUML into B: a tool is developing

SecureUML

USE tool (UML-based Specication Environment)

SecureMova

ArgoUML

ASTD

Maybe StateMachine in Rodin???

ASTD specification by Ocaml?

Topcased Modeler 

CONCERN

What are security properties for an IS???

Access control

Security model refers to Access Control model (paper: Principles of the coupling between UML and formal notations).

ANSWER FROM PROF

Security Properties:

Availability Confidentiality (contains Access Control) Integrity

Availability in RBAC deals with granting permission which will ensure resources are available. RBAC can allow only legitimate users can access the recourse. In other word, RBAC avoids occurring undesirable states in which untrusted users get access to the resource and state but a user is entitled to an access permission cannot get it.

Integrity RBAC deals  with Integrity by controlling who may modify the protected data.

Confidentiality RBAC deals  with Confidentiality by giving access a confidential data only to the authorized users.

my RULES:

SETS -> Class-name + ???(maybe DATA...)

VARIABLES -> Class-variables

INVARIANTS -> Relations between VARIABLES .

INITIALIZATIONS -> Initialize VARIABLES.

OPERATIONS -> Class-methods

QUESTIONS:

Each class is translated to a B-machine correspondingly?

Or depend on the need we can gather several classes?

TOOLS translate SecureUML to B: 

http://b4msecure.forge.imag.fr/

ex - SecureUML concrete model

Define elements in SecureUML Meta-model in B:

SETS -> abstract Classes (like classes in UML)

USERS

ROLES := {DoctorRole, PatientRole}

PERMISSION := {Doctor_Perm, Patient_Perm}

...

INVARIANTS -> Constraint + Relations (variables)

NOTES

Constraints in SecureUML are written in OCL

In fact, I think SecureUML is the way we model functional aspects (UML) and secure aspects. That means SecureUML extends UML  Ex: Class diagraM

SecureUML =

Use ArgoUML to model secureUML is great. However, it's quite slow and not responding sometimes. So I have to close this program and reopen it again. It is annoying.

Anyway, I finished the class diagrams:

Secure Scheduler with secureUML. Link file zargo : https://drive.google.com/file/d/0BwAJPZot1JLvY0ZDSDItU2NwbUU/edit?usp=sharing

P/s: Secure Scheduler is an example in the paper below:

SecureUML- A UML-Based Modeling Language for Model-Driven Security

Medical Record with secureUML and functional diagram: https://drive.google.com/file/d/0BwAJPZot1JLveklFaVlzYzBCYXM/edit?usp=sharing

P/s: Medical Record is an example in the paper below:

It's great! We can use template and modify it online.

1) With UML-B (a UML-like model): It can convert to event-B by using U2B tool (go with UML-B plugin for Rodin) => only need to install UML-B plugin into Rodin -> create UML-B diagrams -> translate to event-B automatically.

I think (Of course, it's not totally UML => then, it cannot cover all aspects (structure or constraints) of UML). Morevoer, event-B also have differences from B-method.

2) With UML in general => what can we do?

SecureMOVA

http://maude.sip.ucm.es/securemova/

ArgoESS - ArgoUML + secureUML plugin

http://sourceforge.net/projects/argouml.mirror/

Install Rodin (currently version 2.8):  http://sourceforge.net/projects/rodin-b-sharp/

To install UML-B plugin: Lanch Rodin -> Help -> Install new software -> choose link Rodin - http://rodin-b-sharp.sourceforge.net/updates -> Modelling Extensions -> choose UML-B Modelling Environment

ProB:  animation and model checking tool for B-method 

http://www.stups.uni-duesseldorf.de/ProB/index.php5/The_ProB_Animator_and_Model_Checker

Atelier B & B-toolkit : proof B

http://www.atelierb.eu/en/

https://github.com/edwardcrichton/BToolkit

UML-B profile: formal modeling notation (UML mapping to B) which supports class diagram.

http://wiki.event-b.org/index.php/Original_UML-B