 |
 |
 |
|
 |
|||
| SSD29 - Formal Specification |
LSE29 - Formal spezifizieren
1 Allocation to V-Model and Methods Allocation
V-Model
SD4.1 - SW Architecture Design
SD4.2 - Design of Internal and External SW Interfaces
SD5.1 - Description of SW Component/Module/Database
Method
2 Brief Characteristics
This service unit defines the requirements for tools used to support the FS - Formal Specification. The different ITSEC requirements depend on the evaluation class. The requirements are described in the document "Criteria for the Development, Realization and Permission of Tools for the Formal Specification and Verification".
A formal specification is required for the formal security model needed with evaluation level E4 according to ITSEC. According to ITSEC, it is also required for the architecture design in level E6.
3 Requirements
3.1 Requirements for Interfaces
| SSD29.I.1 | Granularity | The exchange of control parameters with SWFM01 - Workflow Management is possible for individual closed function packages of the tool by means of a disclosed, documented interface. |
| SSD29.I.2 | Input Interface to SSD23 - Supporting Subsystem Modeling | It is possible to access information about the logical system structure defined with SSD23 via the object management. |
| SSD29.I.3 | Input Interface to SSD24 - Supporting Module Diagrams | It is possible to access information about the module structure defined with SSD24 via the object management. |
| SSD29.I.4 | Input Interface to SSD25 - Supporting Process Diagrams | It is possible to access information about the process structure defined with SSD25 via the object management. |
| SSD29.I.5 | Input Interface to SSD26 - Supporting Use Case Modeling | It is possible to access information about use cases defined with SSD26 via the object management. |
| SSD29.I.6 | Input Interface to SSD27 - Supporting State Modeling in the Object-Oriented Field | It is possible to access information about states, events and actions defined with SSD27 via the object management. |
| SSD29.I.7 | Input Interface to SSD28 - Supporting Interaction Modeling | It is possible to access information about objects and interactions defined with SSD28 via the object management. |
| SSD29.I.8 | Output Interface to SSD30 - Formal Verification | It is possible to have the tool accept the generated formal specification as input for the SSD30 - Formal Verification. |
| SSD29.I.9 | Output Interface to SSD31 - Analysis of Covert Channels | It is possible to have the tool accept the generated formal specification as input for the SSD31 - Analysis of Covert Channels. |
3.2 Requirements for the Methods Support
| SSD29.M.1 | FS - Formal Specification | |
| SSD29.M.1.1 | Formal Specification Language | The tool is adjusted to the used specification language(s). |
| SSD29.M.1.1.1 | Syntax | The specification language has a formally defined syntax. |
| SSD29.M.1.1.2 | Semantics | The specification language has formally defined semantics. If a language construct with various meanings is used, the semantics must be uniquely defined on the basis of the context. |
| SSD29.M.1.1.3 | Expressiveness | The specification language is adjusted to the expressiveness of other utilized languages, in particular to the target language. |
| SSD29.M.1.1.4 | Concepts for the structuring | |
| SSD29.M.1.1.4.1 | Hierarchically Ordered Specification Levels | It is possible to use hierarchically ordered specification levels for the structuring. |
| SSD29.M.1.1.4.2 | Modular Distribution of the Specification | It is possible to use a modular distribution of the specification for the structuring on each specification level. |
| SSD29.M.1.1.5 | Language Constructs for the Specification of Processes | |
| SSD29.M.1.1.5.1 | Sequential and Concurrent Processes | It is possible to specify sequential and concurrent processes. |
| SSD29.M.1.1.5.2 | Process Communication | It is possible to specify the communication between processes. |
| SSD29.M.1.1.6 | Comprehensibility | The formal specification language uses common mathematical symbols and ways of expressions. |
| SSD29.M.1.1.7 | Strict Type Concept | The specification language adheres to a strict type concept. |
3.3 Requirements for Functions
| SSD29.F.1 | Rapid Prototyping | It is possible to execute parts of the specifications defined with method FS or generate source code for the required target language. |
| SSD29.F.2 | Syntax Check | It is possible that the tool checks the syntax of the specification. |
| SSD29.F.3 | Type Check | It is possible that the tool checks the specification with regard to type errors and static semantic (context conditions). |
| SSD29.F.4 | Editor | |
| SSD29.F.4.1 | Entering Formulas |
There are user-friendly resources for the entry of formulas of the formal specification language(s). A uniform, easy-to-handle editor should be available. |
| SSD29.F.4.2 | Structured Representation | It must be easy-to-read, easy to understand and precise. The editor output is context-sensitive. |
| SSD29.F.5 | Formula Collection | There are databases (formula collections) where basic modules like formally specified modules, elementary data structures with corresponding theories, theorems and lemmas are filed that can access the components of the tool. |
3.4 Other Requirements
| SSD29.O.1 | Upward Compatibility | It must be possible to process objects that were generated with an older release of the tool with the later release of that tool, without loss of information and functionality. |
| SSD29.O.2 | Procedural Command Language | The tool has a procedural command language that can be applied by the user to generate and run macros or procedures. |
| SSD29.O.3 | Complexity | There is no limitation of the complexity caused by the tool itself. |
| SSD29.O.4 | Uniform User Interface | |
| SSD29.O.4.1 | The user interface is uniform for all parts of the specification tool. | |
| SSD29.O.4.2 | The user interface of the specification tool and the verification tool are the same. | |
| SSD29.O.5 | Efficiency | Compared with the state of the art, the developments with the tool can be realized in an acceptable time and with acceptable memory requirements. |
| SSD29.O.6 | Installation | |
| SSD29.O.6.1 | Procedure | A procedure for the installation of the specification tool is defined and documented with all parameters. |
| SSD29.O.6.2 | Configuration possibilities | All configuration possibilities for the tool start by the user and the corresponding parameters have been documented, together with the effects on the overall behavior of the tool. |
| SSD29.O.6.3 | Authentication of the binary code | The procedure to guarantee the authentication of the binary code, the installation and the tool start will be described. The procedure to maintenance the tool with the corresponding version control has also been documented. |
| SSD29.O.7 | Documentation | |
| SSD29.O.7.1 | User Documentation | The user documentation addresses a user with know-how of the formal specification and includes all information required for working with the tool. |
| SSD29.O.7.2 | Other Documentation | The methodology used and the mathematical basis are described in detail. |
| SSD29.O.8 | Admission to BSI | For developments according to E5 or E6 in accordance with ITSEC the tool has been accepted by the BSI. |
|
|
|
GDPA Online
Last Updated 01.Jan.2002
Updated by Webmaster
Last Revised 01.Jan.2002
Revised by Webmaster
|