Delain - Deciding language inclusions of open systems
Delain is a tool to decide whether an open system Impl conforms to an open system Spec. For this decision Delain uses the labeled transition systems CSD and BSD created by Chloe.
See the science section for additional information.
Chloe is based on theory introduced in several scientific publications.
Deciding b-Conformance and b-Responsiveness for Open Systems
The labeled transition systems (LTSs) CSD and BSD are created with Chloe based on bounded responsiveness as correctness criterion for the composition of open systems. Delain is then used to decide conformance/responsiveness using the LTS constructed by Chloe. The overall theory is introduced in the following publications:
- Richard Müller, Christian Stahl, Walter Vogler. Deciding conformance for bounded responsiveness. Science of Computer Programming, 2015.
- Richard Müller. Verifying Responsiveness for Open Systems by Means of Conformance Checking. PhD thesis, Technische Universiteit Eindhoven and Humboldt-Universität zu Berlin, 2014.
Improving the comparison of the LTS CSD/BSD
Delain's main function is to read the generated LTSs CSD_b(N) and BSD_b(N) to decide if a composition of two open systems is responsive or if one open system conforms to another open system. The LTS are given as DOT files.
Delain was created to improve the performance for the decision based on given LTS. The optimizations are described here:
- Johannes Dewender. Improving an Implementation for Deciding b-Conformance. Studienarbeit, Humboldt-Universität zu Berlin, 2014.
Delain is open source software, licensed under the AGPL3+.
Installing and running Delain requires a bunch of other tools:
- GCC - The GCC compiler
- Valgrind - Valgrind is an instrumentation framework for building dynamic analysis tools. There are Valgrind tools that can automatically detect many memory management and threading bugs, and profile your programs in detail.
- LCOV - LCOV is a graphical front-end for GCC's coverage testing tool gcov. It collects gcov data for multiple source files and creates HTML pages containing the source code annotated with coverage information.
- Autotools test suite - Part of the GNU Auto-Tools for automated Tests
- flex: The Fast Lexical Analyzer - Flex is a tool for generating scanners. A scanner, sometimes called a tokenizer, is a program which recognizes lexical patterns in text. The flex program reads user-specified input files, or its standard input if no file names are given, for a description of a scanner to generate.
- Bison - Gnu parser generator - Bison is a general-purpose parser generator that converts an annotated context-free grammar into a deterministic LR or generalized LR (GLR) parser employing LALR(1) parser tables.
- GNU Gengetopt - Gengetopt generates a C function that uses getopt_long function to parse the command line options, to validate them and fills a struct .
Extract the tar ball into a folder of your choice, and follow the steps below.
- Test (optional, but recommended)
sudo make install
Delain's manual explains usage, features, and a brief scientifical background. If you are further interested learning more about the science behind Delain, please consult Delain's science section.
Delain's documentation aims at the developer in you. If you are interested in implementation details this is the right place for you to look.
The current maintainer of Delain is Johannes Dewender.
Simon Heiden implemented confCheck/partnerCheck in Chloe, which Delain is based on and Johannes Dewender implemented synthesizing and minimizing CSDs and an optimized parser for Delain.
Several people have committed time, code, and advice to the development of Delain.
- Johannes Dewender (157 commits)
- Simon Heiden (1 commit)
Delain's development team thanks:
- Niels Lohmann for providing the general infrastructure
- Simon Heiden for creating Chloe
- Richard Müller for ideas, help and the theory