Previous Next Functional Tool Requirements Homepage  
System Development Submodel  
SSD30 - Formal Verification  

  LSE30 - Formal verifizieren

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)

    • SD6.1 - Coding of SW Modules

  • SW Modules

    • SD6.2 - Realization of Database

  • Database

    • SD6.3 - Self-Assesment of the SW Module/Database

  • Implementation Document: SW Modules
  • SW Modules
  • Implementation Document: Database
  • Database

    • Method

    DVER - Design Verification
    PVER - Program Verification

    2 Brief Characteristics

    This service unit defines the requirements for tools used to support the "Formal Verification" that a specification is an improvement of another specification (DVER - Design Verification) or that a program meets a specification (PVER - Program Verification). The ITSEC requirements for this tool depend on the various evaluation classes. The requirements have been described in the document "Criteria for the Development, Realization and Admission of Tools for the Formal Specification and Verification". However, the ITSEC require only a formal verification for the formal security model (beginning with evaluation level E4).

    3 Requirements

    3.1 Requirements for Interfaces

    SSD30.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.
    SSD30.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.
    SSD30.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.
    SSD30.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.
    SSD30.I.5 Input Interface to SSD26 - Supporting Use Case Modeling It is possible to access use cases defined with SSD26 via the object management.
    SSD30.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.
    SSD30.I.7 Input Interface to SSD28 - Supporting Interaction Modeling It is possible to access information abut objects and interactions defined with SSD28 via the object management.
    SSD30.I.8 Input Interface to SSD29 - Formal Specification It is possible to have the generated formal specification further processed for formal verification by the tool.
    SSD30.I.9 Input Interface to SSD31 - Analysis of Covert Channels It is possible to have the verification conditions generated in the tool for the analysis of covert channels verified in the Verifier.

    3.2 Requirements for the Methods Support

    SSD30.M.1 DVER - Design Verification
    SSD30.M.1.1 Cooperation of formal methods If several formal methods are used the information about their cooperation with the tool can be exactly proven.
    SSD30.M.1.2 Support of the formal specification language The utilized formal specification language(s) are/will be supported.
    SSD30.M.2 PVER - Program Verification
    SSD30.M.2.1 Cooperation of formal specification and target language Both target language and formal specification language are supported.

    3.3 Requirements for Functions

    SSD30.F.1 Generation of Verification Conditions It is possible to generate verification conditions that can be used to prove that the program meets the specification or that the specification is an improvement. They are created when proving the security model, when improving a specification (DVER) and when proving that a program meets a specification (PVER).
    SSD30.F.2 Simplifier It is possible to automatically prove or simplify the generated verification conditions according to a calculation or default regulation.
    SSD30.F.3 Calculation
    SSD30.F.3.1 Completeness The calculation supports all operators of the specification language and, in addition, for PVER all operator of the target language as well.
    SSD30.F.3.2 Consistence The calculation is not in itself consistent.
    SSD30.F.4 Interactive Verifier
    SSD30.F.4.3 Compatibility All verification conditions generated by the used verification method can be transformed into the input language of the interactive verifier with the help of the tool.
    SSD30.F.4.4 Proof of the Verification Conditions The verifier supports the proof of all verification conditions.
    SSD30.F.4.4.1 Predicate Logic of the first order Verifiers for predicate logic of the first order are possible.
    SSD30.F.4.4.2 Theories Integrated in the Tools Verifiers for the theories integrated into the tool (e. g. natural numbers) are possible.
    SSD30.F.4.4.3 Handling the similarity Similarity handling is possible.
    SSD30.F.4.4.4 Induction verifier Induction verifiers are possible.
    SSD30.F.4.5 Heuristics The tool supports suitable verification heuristics or strategies.
    SSD30.F.4.6 Selection of Rules It is possible to give help about the rules to be applied.
    SSD30.F.5 Editor
    SSD30.F.5.1 Entering formulas There are user-friendly resources for entering verification steps.
    A uniform, easy-to-handle editor should be available.
    SSD30.F.5.2 Structured Representation The context of tool versions is clear. They are easy-to-read, easy to understand and precise. The verification can be followed up by the user. This also means that the applied rules must be entered for the individual verification steps.
    SSD30.F.6 Formula Collections
    SSD30.F.6.1 Database There are databases (formula collections) in which basic modules like formally specified modules, elementary data structures with corresponding theories, theorems and lemmas are filed to which the components of the tool can have access.
    SSD30.F.6.1 Verified/not verified Modules It is possible, to differentiate between verified and not verified modules.
    SSD30.F.7 Protocols All development steps and interactively made user decisions are stored so the user can copy them and this makes error corrections simpler. It is particularly important to define to what extent the specification or the program has been verified.
    SSD30.F.8 Backtracking It is possible to backtrack in a development process to admit new user decisions when required.
    SSD30.F.9 Replay Without interaction with the user the stored development processes are copied and replayed with the tool.

    3.4 Other Requirements

    SSD30.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.
    SSD30.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.
    SSD30.O.3 Complexity There is no limitation of the complexity caused by the tool itself.
    SSD30.O.4 Uniform User Interface
    SSD30.O.4.1 The user interface is uniform for all parts of the specification tool.
    SSD30.O.4.2 The user interface of the specification tool and the verification tool are the same.
    SSD30.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.
    SSD30.O.6 Installation
    SSD30.O.6.1 Procedure A procedure for the installation of the specification tool has been defined and documented with all parameters.
    SSD30.O.6.2 Configuration possibilities All configuration possibilities for the tool start with the user and the corresponding parameters are documented, together with the effects on the overall behavior of the tool.
    SSD30.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 maintain the tool with the corresponding version control has also been documented.
    SSD30.O.7 Documentation
    SSD30.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.
    SSD30.O.7.2 Other Documentation The methodology used and the mathematical basis are minutely described.
    SSD30.O.8 Admission to BSI For developments according to E5 or E6 according to 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