532 \end{center} |
532 \end{center} |
533 |
533 |
534 \noindent |
534 \noindent |
535 Clearly the operating system should only allow to clone a process @{text p} if the |
535 Clearly the operating system should only allow to clone a process @{text p} if the |
536 process is currently alive. The cloned process will get the process |
536 process is currently alive. The cloned process will get the process |
537 ID generated by the function @{term new_proc}. This process ID should |
537 ID ``randomly'' generated by the operating system, but this process ID should |
538 not already exist. Therefore we define @{term new_proc} as *} |
538 not already exist. The admissibility rules for the other events impose similar conditions. |
539 |
|
540 (* HERE ????? chunhan *) |
|
541 text {* |
|
542 \begin{isabelle}\ \ \ \ \ %%% |
|
543 \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
544 @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"} |
|
545 \end{tabular}} |
|
546 \end{isabelle} |
|
547 |
|
548 \noindent |
|
549 namely the highest ID currently in existence increased by one. The |
|
550 admissibility rules for the other events impose similar conditions. |
|
551 |
539 |
552 However, the admissibility check by the operating system is only one |
540 However, the admissibility check by the operating system is only one |
553 ``side'' of the constraints the RC-Model imposes. We also need to |
541 ``side'' of the constraints the RC-Model imposes. We also need to |
554 model the constraints of the access policy. For this we introduce |
542 model the constraints of the access policy. For this we introduce |
555 separate @{text granted}-rules involving the sets @{text |
543 separate @{text granted}-rules involving the sets @{text |
1491 determinated by the efficient forced role of the executable file |
1478 determinated by the efficient forced role of the executable file |
1492 @{term "forcedrole"}. When new process is created, this process' |
1479 @{term "forcedrole"}. When new process is created, this process' |
1493 role is assigned to its creator's role. |
1480 role is assigned to its creator's role. |
1494 |
1481 |
1495 *} |
1482 *} |
|
1483 |
|
1484 |
|
1485 HERE: chunhan |
|
1486 Therefore we define @{term new_proc} as |
|
1487 |
|
1488 (* *) |
|
1489 \begin{isabelle}\ \ \ \ \ %%% |
|
1490 \mbox{\begin{tabular}{l@ {\hspace{2mm}}c@ {\hspace{2mm}}l} |
|
1491 @{term "new_proc s"} & @{text "\<equiv>"} & @{term "Max (current_procs s) + 1"} |
|
1492 \end{tabular}} |
|
1493 \end{isabelle} |
|
1494 |
|
1495 \noindent |
|
1496 namely the highest ID currently in existence increased by one. |
|
1497 |
1496 *) |
1498 *) |