HOL-OCL
/
ocl-examples
Archived
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Added a simple filesystem model.

This commit is contained in:
Achim D. Brucker 2016-10-03 08:11:30 +01:00
parent a6ffc7838e
commit d1e15667b6
5 changed files with 137 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
README.md
View File

@ -14,9 +14,12 @@ projects.
* **[ISP:](./isp)** A simple example of an ISP.
* **[Mini Company:](./mini_company)** A tiny company example modelling a management hierarchy.
* **[Royals and Loyals:](./royals_and_loyals)** The famous royals-and-loyals example.
* **[Simple Filesystem:](./simple_filesystem)** A simple POSIX-like fileystem model.
* **[Stack:](./stack)** A simple stack.
* **[Vehicles:](./vehicles)** A simple modle of vehicles and driver's licenses.
## Team
* [Achim D. Brucker](http://www.brucker.ch/)

9
simple_filesystem/README.md Normal file
View File

@ -0,0 +1,9 @@
# Simple Filesystem
A simple POSIX-like fileystem model.
## Data Sheet
* Format: ArgoUML 0.26
* Language: UML/OCL
For further information (license, citation, etc.), please look at the [README.md](../)
of the main directory.

125
simple_filesystem/simple_filesystem.ocl Normal file
View File

@ -0,0 +1,125 @@
-- Copyright (c) 2003-2007 ETH Zurich, Switzerland
-- 2016 The University of Sheffield, UK
--
-- All rights reserved.
--
-- Redistribution and use in source and binary forms, with or without
-- modification, are permitted provided that the following conditions are met:
--
-- * Redistributions of source code must retain the above copyright notice, this
-- list of conditions and the following disclaimer.
--
-- * Redistributions in binary form must reproduce the above copyright notice,
-- this list of conditions and the following disclaimer in the documentation
-- and/or other materials provided with the distribution.
--
-- THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS"
-- AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE
-- IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
-- DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE
-- FOR ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL
-- DAMAGES (INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR
-- SERVICES; LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER
-- CAUSED AND ON ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY,
-- OR TORT (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
-- OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
--
package simple_filesystem
-------------------------------------------------------------------
-- File --
-------------------------------------------------------------------
context File
inv: File::allInstances()->isUnique(x | x.name)
context File::HasAccess(uid:UID, groups:Set(GROUPID),
p : Permission) : Boolean
post: if owner = uid
then result = perm.owner->includes(p)
else if groups->includes(group)
then result = perm.group->includes(p)
else result = perm.world->includes(p)
-------------------------------------------------------------------
-- User --
-------------------------------------------------------------------
context User
inv: User::allInstances()->forall(x, y |
x.uid = y.uid implies x.groups = y.groups)
context User :: create(n:String)
post: result = File::allInstances@pre()->forall(x | x.name<>n)
post: File::allInstances()->exists(x | x.name=n)
post: result implies File::allInstances()->exists(x |
x.name=n and x.isNewInState() and
x.owner = self.uid and self.groups->includes(x.group) and
x.content = Sequence{} )
post: not result implies File::allInstances()->exists(x |
x.name=n and not x.isNewInState and
x.owner=x.owner@pre and x.group=x.group@pre and
x.content = x.content@pre)
context User :: open(n:String, w:Boolean):Boolean
post: res : result = File::allInstances()->exists(x | x.name=n)
post: write: result and w implies
if has_access(n, W) then
self.curr_fd.isNewInState() and
self.curr_fd.openForWrite and
self.curr_fd.position=0
else self.curr_fd = null
post: read: result and not w implies
if has_access(n, R) then
self.curr_fd.isNewInState() and
not self.curr_fd.openForWrite and
self.curr_fd.position=0
else self.curr_fd = null
post: error: not result implies self.curr_fd = null
context User:: execute(n:String)
pre: has_access(n, X)
post: true -- anything is possible
-- could be extended to a "deep"
-- security property in form of a
-- framing property: anything can change
-- to which the user has access.
context User :: close()
pre: curr_fd <> null
post: curr_fd = null
context User :: appendline(line:String)
pre: curr_fd <> null and curr_fd.openForWrite
post: curr_fd.file.content = curr_fd.AppendLine(line)
and curr_fd.openForWrite = curr_fd.openForWrite@pre
and curr_fd.position = curr_fd.position@pre + 1
context User :: readline(line):String
pre: curr_fd <> null and not curr_fd.openForWrite
post: result = curr_fd.Readline(line)
and curr_fd.openForWrite = curr_fd.openForWrite@pre
and curr_fd.position = curr_fd.position@pre + 1
context User :: updateline(line:String, no:Integer)
pre: curr_fd <> null and curr_fd.openForWrite
post: curr_fd.file.content = curr_fd.Updateline(line,no)
and curr_fd.openForWrite = curr_fd.openForWrite@pre
and curr_fd.position = curr_fd.position@pre + 1
context User :: has_access(n:String,p:Permission) : Boolean
post: result = File::allInstances->exists(x | x.name = n and
x.HasAccess(uid,groups,p))
context User :: chmod(n:String, w:Set(Permission),
g:Set(Permission),
o:Set(Permission))
pre: File::allInstances->exists(x | x.name = n and
x.HasAccess(uid,groups,W))
post: File::allInstances->select(x | x.name=n).perm.world=w
and File::allInstances->select(x | x.name=n).perm.group=g
and File::allInstances->select(x | x.name=n).perm.owner=o
endpackage

BIN
simple_filesystem/simple_filesystem.pdf Normal file
View File

Binary file not shown.

BIN
simple_filesystem/simple_filesystem.zargo Normal file
View File

Binary file not shown.