Bibliographic Details
| Title: |
Rule formats for compositional non-interference properties |
| Authors: |
Tini, Simone1 simone.tini@uninsubria.it |
| Source: |
Journal of Logic & Algebraic Programming. Jul2004, Vol. 60-61, p353-400. 48p. |
| Subjects: |
MARC formats, Machine-readable bibliographic data formats, Polyadic algebras, Computer logic, Program transformation |
| Abstract: |
We introduce the transition rule formats rooted SBSNNI and CP_BNDC. We prove that the non-interference property rooted SBSNNI introduced in the present paper, and the already known non-interference property CP_BNDC, are preserved by constructs of all process algebras with SOS transition rules respecting the restrictions of the formats rooted SBSNNI and CP_BNDC, respectively. To show that our formats have practical applications, we prove that a slight variant of Focardi and Gorrieri''s Security Process Algebra, the Kleene star recursion construct, the replication construct of polyadic π-calculus, and a process algebra extending BPAετ to deal with two level systems, respect both formats. By means of some counterexamples, we prove also that all restrictions of the formats are necessary. [Copyright &y& Elsevier] |
|
Copyright of Journal of Logic & Algebraic Programming is the property of Elsevier B.V. and its content may not be copied or emailed to multiple sites without the copyright holder's express written permission. Additionally, content may not be used with any artificial intelligence tools or machine learning technologies. However, users may print, download, or email articles for individual use. This abstract may be abridged. No warranty is given about the accuracy of the copy. Users should refer to the original published version of the material for the full abstract. (Copyright applies to all Abstracts.) |
| Database: |
Engineering Source |
