About
Modelling Tool
Verification Tool

CoInDiVinE

CoInDiVinE is a Verification Environment for Component-Based Systems which is able to automatically verify component interactions in various types of hierarchical component-based systems using methods of formal verification.

  • Verification Technique

    Formal verification helps to rigorously prove or disprove the correctness of a given system (its model in particular) with respect to a certain formal specification or property. Formal verification in CoIn Verification Environment is realized with the model checking technique. The input of the technique is the model of the system (a CI automaton in our case) and a temporal property we want to check. For properties specification, we use an extended version of the linear temporal logic LTL which we refer to as CI-LTL.

  • CoIn DiVinE in Detail

    CoInDiVinE extends the existing verification environment DiVinE, which is an open source and extensible system for distributed formal verification of concurrent systems. While DiVinE is designed for LTL verification of general systems, CoInDiVinE is meant for formal verification of component-based systems including their specific characteristics.

  • The Main Developers

  • CI-LTL - Linear Temporal Logic for Component Interactions

    CI-LTL is designed to be able to express properties about component interaction (i.e. labels in automata), but also about possible interaction (i.e. label enableness). Therefore, it is both state-based and action-based. CI-LTL uses all standard LTL operators, namely the next-step X, and the until U operator, as well as the standard boolean operators. It has, however, no atomic propositions as their role is played by two operators, E(l) and P(l), where l is a label. Their meaning is informally given as follows.

    • E(l) means "Label l is Enabled" and is true in all states of the system such that the interaction represented by label l can possibly happen.
    • P(l) means "Label l is Proceeding" and is true whenever the interaction represented by label l is actually happening.

    Formal syntax and semantics of the logic can be downloaded here: CI-LTL formally.

  • Download

    • CoInDiVinE itself is included in the current distribution of the DiVinE tool. See the download page for DiVinE.
    • To combine CI automata input files with CI-LTL formulae, you need coin-prop which is available here: coin-prop.tgz. Installation instructions: Simply run make.

  • Usage

    As CoInDiVinE is included in DiVinE, its usage is similar to DiVinE's, with the following differences:
    • The input files are to be written in CoIn textual notation.
    • The CI-LTL logical formula is to be written in CI-LTL textual notation. The formula is to be transformed into property automaton and added to the model using the coin-prop tool (see above) as follows:

      The binary takes two arguments: the first is either the word weak or strong which determines whether weak or strong CI-LTL formula will be given. The second is the name of the file with the model that should be completed with the property automaton, i.e. for example:

      ./coin-prop strong coffee.coin

      The user is then asked to supply the formula:

      Enter CI-LTL formula: G F E(2, money, 1a)

      Then, if the chosen logic was weak CI-LTL, the user is asked to supply the interesting action labels, one on a line, ending the list with an empty line. Note that the action labels from P() and U() subformulae of the formula are always included so they do not need to be supplied this way.

      The resulting property automaton is added to the model and stored in a new file with the extension .prop.coin, i.e. if the original file with the model was coffee.coin, the new file with the property automaton would be coffee.prop.coin.