---
title: CPFSTool Metamodel
...


```{.clafer}
//CPFSTool Metamodel

abstract SecurityProblemFrame
    name : string 
    intent : string 
    informalDescription : string 
    effect -> Effect 
    spfFrameDiagram -> FrameDiagram 

abstract ConcretizedSecurityProblemFrame
    name : string 
    intent : string 
    informalDescription : string 
    cspfFrameDiagram -> FrameDiagram 
    necessaryCondition -> NecessaryCondition *

abstract FrameDiagram
    domains -> Domain 3..*
    interfaces -> Interface 2..*
    requirementReferences -> RequirementReference 2..*
    requirementTemplate -> RequirementTemplate 
    [some d:domains|d.isMachine]
    [some i:interfaces|some d:domains|some m:domains|(m.isMachine && i in m.isConnectedBy && i in d.isConnectedBy)]
    [some i:interfaces|(some d:i.connects|d.isMachine)&&(some p:i.contains|p.isControlledBy.isMachine)]
    [all d:domains|some i:interfaces|i in d.isConnectedBy]
    [all d:domains|all p:d.controls|some i:d.isConnectedBy|p in i.contains]
    [all d:domains|d.isConnectedBy in interfaces]
    [some d:domains|(no d.isMachine => d.isConstrainedByUsing in requirementReferences)]
    [all disj d1;d2:domains|d1.name.ref != d2.name.ref]
    [all disj d1;d2:domains|d1.abbreviation.ref != d2.abbreviation.ref] 
    [all d:domains|all i:interfaces|all p:i.contains|p.name != d.name]
    [all i:interfaces|i.connects in domains]
    [all i:interfaces|all p:i.contains|one d:domains|p in d.controls && d in i.connects]
    [requirementTemplate.constrainsUsing in requirementReferences]
    [requirementReferences in requirementTemplate.refersToUsing]
    [all rr:requirementReferences|rr.isConnectedToReq = requirementTemplate]
    [all rr:requirementReferences|rr.isConnectedToDomain in domains]

abstract Effect
    formulaE -> Formula +

abstract NecessaryCondition
    formulaNC -> Formula +

abstract Formula
    content : string 
    informalDescription : string 

abstract Domain
    name : string 
    abbreviation : string 
    isGiven ?
    isMachine ?
    controls -> InterfacePhenomenon *
        [parent in this.isControlledBy]
    isConstrainedByUsing -> ConstrainingRequirementReference ?
    isReferredToByUsing -> RequirementReference ?
        [parent in this.isConnectedToDomain]
    isConnectedBy -> Interface +
        [parent in this.connects]
    [isMachine => no isGiven]
    [isMachine => no isReferredToByUsing]
    [isMachine => no isConstrainedByUsing]

abstract CausalDomain : Domain 

abstract BiddableDomain : Domain
    [isGiven]
    [no isMachine]
    [no isConstrainedByUsing]

abstract LexicalDomain : CausalDomain 
    [no isMachine]

abstract DisplayDomain : CausalDomain 

abstract Interface
    name : string 
    contains -> InterfacePhenomenon +
    connects -> Domain 2..*
        [parent in this.isConnectedBy]
    [all p:contains|one d:connects|p.isControlledBy = d]

enum PhenomenonType = causal | symbolic | event

abstract Phenomenon
    name : string 
    type -> PhenomenonType 

abstract InterfacePhenomenon : Phenomenon 
    isControlledBy -> Domain 
        [parent in this.controls]
    isContainedInIf -> Interface +
        [parent in this.contains]
    [isControlledBy in isContainedInIf.connects]


abstract RequirementPhenomenon : Phenomenon 

abstract RequirementTemplate
    content : string 
    constrainsUsing -> ConstrainingRequirementReference +
    refersToUsing -> RequirementReference *
        [parent in this.isConnectedToReq]

abstract RequirementReference
    name : string 
    contains -> RequirementPhenomenon +
    isConnectedToReq -> RequirementTemplate 
        [parent in this.refersToUsing]
    isConnectedToDomain -> Domain 
        [parent in this.isReferredToByUsing]
    [no isConnectedToDomain.isMachine]

abstract ConstrainingRequirementReference : RequirementReference 
    related -> SecurityProblemFrame *
    refined -> SecurityProblemFrame *
    [no isConnectedToDomain.isMachine]


```

```{.clafer .summary}
```