HOL-OCL
/
su4sml
1
0
Fork 0
Code Issues Pull Requests Releases Activity

some cleanup 

git-svn-id: https://projects.brucker.ch/su4sml/svn/infsec-import/trunk/src/su4sml@4448 3260e6d1-4efc-4170-b0a7-36055960796d
This commit is contained in:
Jürgen Doser 2006-04-27 14:27:16 +00:00
parent 76f9ee17e7
commit e9a24cfac6
21 changed files with 418 additions and 456 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
src/codegen/base_cartridge.sml
View File

@ -21,6 +21,30 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
(**
* This cartridge knows about the basic elements of UML class diagrams.
* The elements are classifiers, attributes, and operations with their
* parameters in terms of the Rep interface
*)
signature BASE_CARTRIDGE =
sig
include CARTRIDGE
(** returns the current classifier. *)
val curClassifier: environment -> Rep.Classifier option
(** returns the current attribute *)
val curAttribute: environment -> Rep.attribute option
(** returns the current operation *)
val curOperation: environment -> Rep.operation option
(** returns the current operation parameter *)
val curArgument : environment -> (string * Rep_OclType.OclType) option
end
structure Base_Cartridge : BASE_CARTRIDGE =
struct
(* translation functions *)

6
src/codegen/componentuml_cartridge.sml
View File

@ -1,12 +1,8 @@
functor ComponentUML_Cartridge(SuperCart : SECURITY_LANGUAGE_CARTRIDGE) : DESIGN_LANGUAGE_CARTRIDGE =
functor ComponentUML_Cartridge(SuperCart : SECUREUML_CARTRIDGE) : DESIGN_LANGUAGE_CARTRIDGE =
struct
structure Design = ComponentUML
(* TODO: fill out *)
type environment = { extension: SuperCart.environment}
type Model = SuperCart.Model

37
src/codegen/secureuml_cartridge.sml
View File

@ -24,6 +24,25 @@
******************************************************************************)
signature SECUREUML_CARTRIDGE =
sig
(** the particular secureuml dialect used *)
structure Security:SECURITY_LANGUAGE
include BASE_CARTRIDGE where
type Model = Rep.Classifier list * Security.Configuration
val curPermissionSet: environment -> Security.Permission list option
val curPermission : environment -> Security.Permission option
val curRole : environment -> string option
val curConstraint : environment -> Rep_OclTerm.OclTerm option
val isInPermission : Security.Design.Action -> Security.Permission -> bool
end
functor SecureUML_Cartridge(structure SuperCart : BASE_CARTRIDGE;
structure D: DESIGN_LANGUAGE)
: SECUREUML_CARTRIDGE =
@ -40,7 +59,6 @@ type environment = { model : Model,
curConstraint : Rep_OclTerm.OclTerm option,
extension : SuperCart.environment }
fun getPermissions conf = Security.getPermissions conf
(* service functions for other cartridges to have access to the current
* list items
@ -56,13 +74,16 @@ fun curPermission' (env : environment) = Option.valOf (#curPermission env)
fun curRole' (env : environment) = Option.valOf (#curRole env)
fun curConstraint' (env : environment) = Option.valOf (#curConstraint env)
fun initEnv model = { model = Security.parse model,
curPermissionSet = NONE,
curPermission = NONE,
curRole = NONE,
curConstraint = NONE,
extension = SuperCart.initEnv model } : environment
fun initEnv model = let val m = Security.parse model
in
{ model = m,
curPermissionSet = NONE,
curPermission = NONE,
curRole = NONE,
curConstraint = NONE,
extension = SuperCart.initEnv (#1 m) } : environment
end
(* unpack : environment -> SuperCart.environment *)
fun unpack (env : environment) = #extension env

18
src/codegen/tpl_parser.sml
View File

@ -21,6 +21,24 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature TPL_PARSER =
sig
datatype TemplateTree
= ElseNode of TemplateTree list
| EvalLeaf of TemplateTree list
| ForEachNode of string * TemplateTree list
| IfNode of string * TemplateTree list
| OpenFileLeaf of string
| RootNode of TemplateTree list
| TextLeaf of string
val printTTree : TemplateTree -> unit
val parse : string -> TemplateTree
end
structure Tpl_Parser : TPL_PARSER =
struct
open Gcg_Helper

24
src/component_uml.sml
View File

@ -24,8 +24,30 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature COMPONENTUML =
sig
datatype Resource = Entity of Rep.Classifier
| EntityMethod of Rep.operation
| EntityAttribute of Rep.attribute
val contained_resources : Resource -> Resource list
datatype Action = SimpleAction of string * Resource
| CompositeAction of string * Resource
(* val action_names: string list *)
val subordinated_actions: Action -> Action list
val actions_of : Resource -> Action list
val resource_of: Action -> Resource
end
(** ComponentUML is a simple language for component-based modeling. *)
structure ComponentUML (* : DESIGN_LANGUAGE*) =
structure ComponentUML : COMPONENTUML =
struct
(** The type of resource, plus a path name specifiying the resource.

27
src/mds.sig
View File

@ -24,8 +24,10 @@
******************************************************************************)
(* a design language specifies what the protected resources and the *)
(* possible actions on these resources are *)
(**
* a design language specifies what the protected resources and the
* possible actions on these resources are.
*)
signature DESIGN_LANGUAGE =
sig
@ -48,9 +50,11 @@ sig
end
(* A security language speaks about users, and their permissions: *)
(* at this level, this is completeley independent of the access *)
(* control model used in the application *)
(**
* A security language speaks about users, and their permissions.
* at this level, this is completeley independent of the access
* control model used in the application
*)
signature SECURITY_LANGUAGE =
sig
structure Design : DESIGN_LANGUAGE
@ -58,15 +62,15 @@ sig
type Configuration
type Config_Type = string
val type_of : Configuration -> Config_Type
val is_empty: Configuration -> bool
eqtype Permission
val getPermissions : Configuration -> Permission list
val type_of : Configuration -> Config_Type
val is_empty : Configuration -> bool
type User
val name_of : User -> string
eqtype Permission
val getPermissions : Configuration -> Permission list
(* a bit unclear, which of the following we really need *)
val users_of : Permission -> User list
(* val permissions_of : User -> Permission list *)
@ -75,7 +79,8 @@ sig
val actions_of : Permission -> Design.Action list
val permissions_of : Design.Action -> Permission list
val parse: Rep_Core.Classifier list -> (Rep_Core.Classifier list * Configuration)
val parse: Rep_Core.Classifier list ->
(Rep_Core.Classifier list * Configuration)
end

29
src/mds_parser.sig
View File

@ -1,29 +0,0 @@
(*****************************************************************************
* su4sml - a SecureUML repository for SML
*
* mds_parser.sig - signature for mds-parser for the import interface
* Copyright (C) 2005 Achim D. Brucker <brucker@inf.ethz.ch>
* Jürgen Doser <doserj@inf.ethz.ch>
*
* This file is part of su4sml.
*
* su4sml is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* su4sml is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature MDS_PARSER =
sig
val list_classes : string -> mdr_encoder.Classifier list
end

32
src/rep.sig
View File

@ -1,32 +0,0 @@
(*****************************************************************************
* su4sml - a SecureUML repository for SML
*
* sc_import.sig - generic state diagram import signature for su4sml
* Copyright (C) 2005 Achim D. Brucker <brucker@inf.ethz.ch>
* Jürgen Doser <doserj@inf.ethz.ch>
*
* This file is part of su4sml.
*
* su4sml is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* su4sml is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP =
sig
include REP_CORE
include REP_ACTIVITY_GRAPH
type Model = Rep_Core.Classifier list
end

9
src/rep.sml
View File

@ -22,6 +22,15 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP =
sig
include REP_CORE
include REP_ACTIVITY_GRAPH
type Model = Classifier list
end
structure Rep : REP =
struct

32
src/rep_activity_graphs.sig
View File

@ -1,32 +0,0 @@
(*****************************************************************************
* su4sml - a SecureUML repository for SML
*
* state_machine.sig - generic state machines
* Copyright (C) 2005 Achim D. Brucker <brucker@inf.ethz.ch>
* Jürgen Doser <doserj@inf.ethz.ch>
* Burkhart Wolff <bwolff@inf.ethz.ch>
*
* This file is part of su4sml.
*
* su4sml is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* su4sml is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP_ACTIVITY_GRAPH =
sig
include REP_STATE_MACHINE
type ActivityGraph = StateMachine
end

8
src/rep_activity_graphs.sml
View File

@ -23,6 +23,14 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP_ACTIVITY_GRAPH =
sig
include REP_STATE_MACHINE
type ActivityGraph = StateMachine
end
structure Rep_ActivityGraph : REP_ACTIVITY_GRAPH =
struct
open Rep_StateMachine

124
src/rep_core.sig
View File

@ -1,124 +0,0 @@
(*****************************************************************************
* su4sml - a SecureUML repository for SML
*
* mdr_core.sig - generic meta data repository import signature for su4sml
* Copyright (C) 2001-2005 Achim D. Brucker <brucker@inf.ethz.ch>
* Burkhart Wolff <bwolff@inf.ethz.ch>
*
* This file is part of su4sml.
*
* su4sml is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* su4sml is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP_CORE =
sig
type Scope
type Visibility
type operation = { name : string,
precondition : (string option * Rep_OclTerm.OclTerm) list,
postcondition : (string option * Rep_OclTerm.OclTerm) list,
arguments : (string * Rep_OclType.OclType) list,
result : Rep_OclType.OclType,
isQuery : bool,
scope : Scope,
visibility : Visibility
}
type associationend = {name : string,
aend_type : Rep_OclType.OclType,
multiplicity: (int * int) list,
ordered: bool,
visibility: Visibility,
init: Rep_OclTerm.OclTerm option
}
type attribute = {
name : string,
attr_type : Rep_OclType.OclType,
visibility : Visibility,
scope: Scope,
init : Rep_OclTerm.OclTerm option
}
datatype Classifier =
Class of
{ name : Rep_OclType.Path,
parent : Rep_OclType.Path option,
attributes : attribute list,
operations : operation list,
associationends : associationend list,
invariant : (string option * Rep_OclTerm.OclTerm) list,
stereotypes : string list,
interfaces : Rep_OclType.Path list,
thyname : string option,
activity_graphs : Rep_ActivityGraph.ActivityGraph list
}
| Interface of (* not supported yet *)
{ name : Rep_OclType.Path,
parents : Rep_OclType.Path list,
operations : operation list,
stereotypes : string list,
invariant : (string option * Rep_OclTerm.OclTerm) list,
thyname : string option
}
| Enumeration of (* not really supported yet? *)
{ name : Rep_OclType.Path,
parent : Rep_OclType.Path option,
operations : operation list,
literals : string list,
invariant : (string option * Rep_OclTerm.OclTerm) list,
stereotypes : string list,
interfaces : Rep_OclType.Path list,
thyname : string option
}
| Primitive of (* not really supported yet *)
{ name : Rep_OclType.Path,
parent : Rep_OclType.Path option,
operations : operation list,
associationends : associationend list,
invariant : (string option * Rep_OclTerm.OclTerm) list,
stereotypes : string list,
interfaces : Rep_OclType.Path list,
thyname : string option
}
val OclAnyC : Classifier
val normalize : Classifier -> Classifier
val normalize_init : Classifier -> Classifier
val name_of : Classifier -> Rep_OclType.Path
val package_of : Classifier -> Rep_OclType.Path
val short_name_of : Classifier -> string
val parent_name_of : Classifier -> Rep_OclType.Path
val parent_package_of : Classifier -> Rep_OclType.Path
val short_parent_name_of : Classifier -> string
val thy_name_of : Classifier -> string
val update_thyname : string -> Classifier -> Classifier
val attributes_of : Classifier -> attribute list
val operations_of : Classifier -> operation list
val invariant_of : Classifier -> (string option * Rep_OclTerm.OclTerm) list
val string_of_path : string list -> string
val arguments_of_op : operation -> (string * Rep_OclType.OclType) list
val precondition_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val result_of_op : operation -> Rep_OclType.OclType
val postcondition_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val name_of_op : operation -> string
val mangled_name_of_op : operation -> string
end

101
src/rep_core.sml
View File

@ -22,6 +22,107 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP_CORE =
sig
type Scope
type Visibility
type operation = { name : string,
precondition : (string option * Rep_OclTerm.OclTerm) list,
postcondition : (string option * Rep_OclTerm.OclTerm) list,
arguments : (string * Rep_OclType.OclType) list,
result : Rep_OclType.OclType,
isQuery : bool,
scope : Scope,
visibility : Visibility
}
type associationend = {name : string,
aend_type : Rep_OclType.OclType,
multiplicity: (int * int) list,
ordered: bool,
visibility: Visibility,
init: Rep_OclTerm.OclTerm option
}
type attribute = {
name : string,
attr_type : Rep_OclType.OclType,
visibility : Visibility,
scope: Scope,
init : Rep_OclTerm.OclTerm option
}
datatype Classifier =
Class of
{ name : Rep_OclType.Path,
parent : Rep_OclType.Path option,
attributes : attribute list,
operations : operation list,
associationends : associationend list,
invariant : (string option * Rep_OclTerm.OclTerm) list,
stereotypes : string list,
interfaces : Rep_OclType.Path list,
thyname : string option,
activity_graphs : Rep_ActivityGraph.ActivityGraph list
}
| Interface of (* not supported yet *)
{ name : Rep_OclType.Path,
parents : Rep_OclType.Path list,
operations : operation list,
stereotypes : string list,
invariant : (string option * Rep_OclTerm.OclTerm) list,
thyname : string option
}
| Enumeration of (* not really supported yet? *)
{ name : Rep_OclType.Path,
parent : Rep_OclType.Path option,
operations : operation list,
literals : string list,
invariant : (string option * Rep_OclTerm.OclTerm) list,
stereotypes : string list,
interfaces : Rep_OclType.Path list,
thyname : string option
}
| Primitive of (* not really supported yet *)
{ name : Rep_OclType.Path,
parent : Rep_OclType.Path option,
operations : operation list,
associationends : associationend list,
invariant : (string option * Rep_OclTerm.OclTerm) list,
stereotypes : string list,
interfaces : Rep_OclType.Path list,
thyname : string option
}
val OclAnyC : Classifier
val normalize : Classifier -> Classifier
val normalize_init : Classifier -> Classifier
val name_of : Classifier -> Rep_OclType.Path
val package_of : Classifier -> Rep_OclType.Path
val short_name_of : Classifier -> string
val parent_name_of : Classifier -> Rep_OclType.Path
val parent_package_of : Classifier -> Rep_OclType.Path
val short_parent_name_of : Classifier -> string
val thy_name_of : Classifier -> string
val update_thyname : string -> Classifier -> Classifier
val attributes_of : Classifier -> attribute list
val operations_of : Classifier -> operation list
val invariant_of : Classifier -> (string option * Rep_OclTerm.OclTerm) list
val string_of_path : string list -> string
val arguments_of_op : operation -> (string * Rep_OclType.OclType) list
val precondition_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val result_of_op : operation -> Rep_OclType.OclType
val postcondition_of_op : operation -> (string option * Rep_OclTerm.OclTerm) list
val name_of_op : operation -> string
val mangled_name_of_op : operation -> string
end
structure Rep_Core : REP_CORE =
struct
open library

83
src/rep_ocl.sig
View File

@ -1,83 +0,0 @@
(*****************************************************************************
* su4sml - a SecureUML repository for SML
*
* ocl.sig -
* Copyright (C) 2001-2005 Achim D. Brucker <brucker@inf.ethz.ch>
* Burkhart Wolff <bwolff@inf.ethz.ch>
*
* This file is part of su4sml.
*
* su4sml is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* su4sml is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP_OCL_TYPE =
sig
type Path = string list
datatype OclType = Integer | Real | String | Boolean | OclAny
| Set of OclType | Sequence of OclType
| OrderedSet of OclType | Bag of OclType
| Collection of OclType
| Classifier of Path | OclVoid | DummyT
val string_of_OclType : OclType -> string
val string_of_path : Path -> string
end
signature REP_OCL_TERM =
sig
include REP_OCL_TYPE
datatype OclTerm =
Literal of string * OclType (* Literal with type *)
| CollectionLiteral of CollectionPart list * OclType (* content with type *)
| If of OclTerm * OclType (* condition *)
* OclTerm * OclType (* then *)
* OclTerm * OclType (* else *)
* OclType (* result type *)
| AssociationEndCall of OclTerm * OclType (* source *)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AttributeCall of OclTerm * OclType (* source *)
* Path (* attribute *)
* OclType (* result type *)
| OperationCall of OclTerm * OclType (* source *)
* Path (* operation *)
* (OclTerm * OclType) list (* parameters *)
* OclType (* result tupe *)
| OperationWithType of OclTerm * OclType (* source *)
* string * OclType (* type parameter *)
* OclType (* result type *)
| Variable of string * OclType (* name with type *)
| Let of string * OclType (* variable *)
* OclTerm * OclType (* rhs *)
* OclTerm * OclType (* in *)
| Iterate of (string * OclType) list (* iterator variables *)
* string * OclType * OclTerm (* result variable *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator body *)
* OclType (* result type *)
| Iterator of string (* name of iterator *)
* (string * OclType) list (* iterator variables *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator-body *)
* OclType (* result type *)
and CollectionPart = CollectionItem of OclTerm * OclType
| CollectionRange of OclTerm (* first *)
* OclTerm (* last *)
* OclType
end

61
src/rep_ocl.sml
View File

@ -22,6 +22,67 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP_OCL_TYPE =
sig
type Path = string list
datatype OclType = Integer | Real | String | Boolean | OclAny
| Set of OclType | Sequence of OclType
| OrderedSet of OclType | Bag of OclType
| Collection of OclType
| Classifier of Path | OclVoid | DummyT
val string_of_OclType : OclType -> string
val string_of_path : Path -> string
end
signature REP_OCL_TERM =
sig
include REP_OCL_TYPE
datatype OclTerm =
Literal of string * OclType (* Literal with type *)
| CollectionLiteral of CollectionPart list * OclType (* content with type *)
| If of OclTerm * OclType (* condition *)
* OclTerm * OclType (* then *)
* OclTerm * OclType (* else *)
* OclType (* result type *)
| AssociationEndCall of OclTerm * OclType (* source *)
* Path (* assoc.-enc *)
* OclType (* result type *)
| AttributeCall of OclTerm * OclType (* source *)
* Path (* attribute *)
* OclType (* result type *)
| OperationCall of OclTerm * OclType (* source *)
* Path (* operation *)
* (OclTerm * OclType) list (* parameters *)
* OclType (* result tupe *)
| OperationWithType of OclTerm * OclType (* source *)
* string * OclType (* type parameter *)
* OclType (* result type *)
| Variable of string * OclType (* name with type *)
| Let of string * OclType (* variable *)
* OclTerm * OclType (* rhs *)
* OclTerm * OclType (* in *)
| Iterate of (string * OclType) list (* iterator variables *)
* string * OclType * OclTerm (* result variable *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator body *)
* OclType (* result type *)
| Iterator of string (* name of iterator *)
* (string * OclType) list (* iterator variables *)
* OclTerm * OclType (* source *)
* OclTerm * OclType (* iterator-body *)
* OclType (* result type *)
and CollectionPart = CollectionItem of OclTerm * OclType
| CollectionRange of OclTerm (* first *)
* OclTerm (* last *)
* OclType
end
structure Rep_OclType : REP_OCL_TYPE =
struct
open library

12
src/rep_secure.sig
View File

@ -24,12 +24,20 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
(** a repository for uml models equipped with a security language *)
signature REP_SECURE =
sig
(** the security language used. *)
structure Security : SECURITY_LANGUAGE
(**
* a "secure repository" model consist of a repository model
* plus a security configuration.
*)
type Model = Rep_Core.Classifier list * Security.Configuration
(** *)
val readXMI: string -> Model
end

19
src/rep_secure.sml
View File

@ -25,6 +25,25 @@
******************************************************************************)
(** a repository for uml models equipped with a security language *)
signature REP_SECURE =
sig
(** the security language used. *)
structure Security : SECURITY_LANGUAGE
(**
* a "secure repository" model consist of a repository model
* plus a security configuration.
*)
type Model = Rep_Core.Classifier list * Security.Configuration
(** *)
val readXMI: string -> Model
end
functor Rep_Secure(structure Security : SECURITY_LANGUAGE) : REP_SECURE =
struct
structure Security = Security

112
src/rep_state_machines.sig
View File

@ -1,112 +0,0 @@
(*****************************************************************************
* su4sml - a SecureUML repository for SML
*
* state_machine.sig - generic state machines
* Copyright (C) 2005 Achim D. Brucker <brucker@inf.ethz.ch>
* Jürgen Doser <doserj@inf.ethz.ch>
* Burkhart Wolff <bwolff@inf.ethz.ch>
*
* This file is part of su4sml.
*
* su4sml is free software; you can redistribute it and/or modify it under
* the terms of the GNU General Public License as published by the Free
* Software Foundation; either version 2 of the License, or (at your option)
* any later version.
*
* su4sml is distributed in the hope that it will be useful, but WITHOUT ANY
* WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS
* FOR A PARTICULAR PURPOSE. See the GNU General Public License for more
* details.
*
* You should have received a copy of the GNU General Public License along
* with this program; if not, write to the Free Software Foundation, Inc.,
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP_STATE_MACHINE =
sig
type StateVertex_Id
type Transition_Id
datatype Procedure = Proc_mk of {proc_id : string,
language : string,
body : string,
expression : string }
(* perhaps this type has to be changes according to what we can expect *)
(* from CASE tools *)
type Guard = Rep_OclTerm.OclTerm
type Parameter = string * Rep_OclType.OclType
datatype Event = SignalEvent of Parameter list
| CallEvent of Rep_OclType.Path * Parameter list
(* | TimeEvent of Parameter list *)
(* | ChangeEvent of Parameter list *)
datatype Transition = T_mk of {trans_id: Transition_Id,
source : StateVertex_Id,
target : StateVertex_Id,
guard : Guard option,
trigger : Event option,
effect : Procedure option
(* mmm : StateVertexId option *)
}
type PseudoStateVars = XMI_StateMachines.PseudoStateVars
datatype StateVertex =
State_CompositeState
of {name : string,
state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list,
subvertex : StateVertex list,
isConcurrent : bool
(* submachine : StateMachine *
{isDynamic : bool
(* + dynamicArguments
+ dynamicMultiplicity *)} option *)}
(* variant for Subactivity State *)
| State_SimpleState
of {name : string,
state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list}
| SimpleState_ActionState (* from ActivityGraphs *)
of {name : string,
state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list,
isDynamic : bool
(* + dynamicArguments + dynamicMultiplicity *)}
| SimpleState_ObjectflowState (* from ActivityGraphs *)
of {state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list,
isSynch : bool,
parameter : Parameter list,
types : Rep_OclType.Path list (* Classifier_Id *)}
| State_FinalState
of {state_id : StateVertex_Id,
incoming : Transition_Id list}
| PseudoState
of {state_id : StateVertex_Id,
kind : PseudoStateVars,
outgoing : Transition_Id list,
incoming : Transition_Id list}
| SyncState
of {state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list}
(* | StubState *)
and StateMachine = SM_mk of {top : StateVertex,
transition : Transition list}
end

88
src/rep_state_machines.sml
View File

@ -23,6 +23,94 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
signature REP_STATE_MACHINE =
sig
type StateVertex_Id
type Transition_Id
datatype Procedure = Proc_mk of {proc_id : string,
language : string,
body : string,
expression : string }
(* perhaps this type has to be changes according to what we can expect *)
(* from CASE tools *)
type Guard = Rep_OclTerm.OclTerm
type Parameter = string * Rep_OclType.OclType
datatype Event = SignalEvent of Parameter list
| CallEvent of Rep_OclType.Path * Parameter list
(* | TimeEvent of Parameter list *)
(* | ChangeEvent of Parameter list *)
datatype Transition = T_mk of {trans_id: Transition_Id,
source : StateVertex_Id,
target : StateVertex_Id,
guard : Guard option,
trigger : Event option,
effect : Procedure option
(* mmm : StateVertexId option *)
}
type PseudoStateVars = XMI_StateMachines.PseudoStateVars
datatype StateVertex =
State_CompositeState
of {name : string,
state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list,
subvertex : StateVertex list,
isConcurrent : bool
(* submachine : StateMachine *
{isDynamic : bool
(* + dynamicArguments
+ dynamicMultiplicity *)} option *)}
(* variant for Subactivity State *)
| State_SimpleState
of {name : string,
state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list}
| SimpleState_ActionState (* from ActivityGraphs *)
of {name : string,
state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list,
isDynamic : bool
(* + dynamicArguments + dynamicMultiplicity *)}
| SimpleState_ObjectflowState (* from ActivityGraphs *)
of {state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list,
isSynch : bool,
parameter : Parameter list,
types : Rep_OclType.Path list (* Classifier_Id *)}
| State_FinalState
of {state_id : StateVertex_Id,
incoming : Transition_Id list}
| PseudoState
of {state_id : StateVertex_Id,
kind : PseudoStateVars,
outgoing : Transition_Id list,
incoming : Transition_Id list}
| SyncState
of {state_id : StateVertex_Id,
outgoing : Transition_Id list,
incoming : Transition_Id list}
(* | StubState *)
and StateMachine = SM_mk of {top : StateVertex,
transition : Transition list}
end
structure Rep_StateMachine : REP_STATE_MACHINE =
struct

9
src/secure_uml.sml
View File

@ -23,8 +23,11 @@
* 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
******************************************************************************)
(** SecureUML is a simple security language, based on RBAC, where permissions *)
(* can be further constrained using OCL: *)
(**
* SecureUML is a simple security language based on RBAC.
* Permissions relate roles with actions and can be further constrained
* using OCL:
*)
functor SecureUML(structure Design: DESIGN_LANGUAGE):SECURITY_LANGUAGE =
struct
@ -82,6 +85,7 @@ fun stereotypes_of (Rep.Class {stereotypes,...}) = stereotypes
| stereotypes_of (Rep.Primitive {stereotypes,...}) = stereotypes
| stereotypes_of (Rep.Interface {stereotypes,...}) = stereotypes
fun has_no_stereotype strings c =
not (List.exists (fn stereotype => List.exists (fn x => x = stereotype)
strings) (stereotypes_of c))
@ -89,6 +93,7 @@ fun has_no_stereotype strings c =
fun has_stereotype string c =
List.exists (fn x => x=string) (stereotypes_of c)
fun filter_permission cs = List.filter (has_stereotype "Permission") cs
(* FIXME: handle groups also *)
fun filter_subject cs = List.filter (has_stereotype "User") cs

19
src/su4sml.cm
View File

@ -7,20 +7,14 @@ Group is
#endif
../lib/fxp/src/fxlib.cm
library.sml
rep_ocl.sig
rep_ocl.sml
rep_state_machines.sig
rep_state_machines.sml
rep_activity_graphs.sig
rep_activity_graphs.sml
rep_core.sig
rep_core.sml
mds.sig
secure_uml.sml
component_uml.sml
rep_secure.sig
rep_secure.sml
rep.sig
rep.sml
xmi_ocl.sml
xmi_core.sml
@ -38,18 +32,13 @@ Group is
codegen/compiler/smlnj.sml
codegen/gcg_library.sml
codegen/gcg_helper.sml
codegen/tpl_parser.sig
codegen/tpl_parser.sml
codegen/cartridge.sig
codegen/security_cartridge.sig
codegen/base_cartridge.sig
codegen/cartridge.sig
codegen/base_cartridge.sml
codegen/c#_cartridge.sml
codegen/c#_net1_cartridge.sml
codegen/secureuml_cartridge.sig
codegen/secureuml_cartridge.sml
codegen/gcg_core.sig
codegen/gcg_core.sml
codegen/codegen.sml
codegen/design_cartridge.sig
codegen/componentuml_cartridge.sml
codegen/design_cartridge.sig
codegen/gcg_core.sml
codegen/codegen.sml