Previous Next Functional Tool Requirements Homepage  
System Development Submodel  
SSD29 - Formal Specification  

  LSE29 - Formal spezifizieren

Contents  
  • 1 Allocation to V-Model and Methods Allocation
  • 2 Brief Characteristics
  • 3 Requirements
  •       3.1 Requirements for Interfaces
  •       3.2 Requirements for the Methods Support
  •       3.3 Requirements for Functions
  •       3.4 Other Requirements
  • 1 Allocation to V-Model and Methods Allocation

    V-Model

    SD2.5 - Interface Description

  • Interface Description.Description of the Interfaces
  • SD4.1 - SW Architecture Design

  • SW Architecture.Solution Proposals
  • SW Architecture.Modularization/Database Design
  • SW Architecture.Interfaces
  • Interface Overview.System-Internal Interfaces
  • SD4.2 - Design of Internal and External SW Interfaces

  • Interface Description.Description of the Interfaces
  • SD5.1 - Description of SW Component/Module/Database

  • SW Design (Database).Database Description
  • SW Design (Module).SW Component/SW Module Description (in object-oriented Databases)
  • Method

    FS - Formal Specification

    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.

    Previous Next GDPA Online Last Updated 01.Jan.2002 Updated by Webmaster Last Revised 01.Jan.2002 Revised by Webmaster