Chloe - Characterizing languages of open systems
Chloe is a tool to create the labeled transitions systems CSD and BSD to decide bounded responsiveness with Delain.
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 created with Chloe are part of a theory to decide if compositions of open systems are correct. The correctness criterion is bounded responsiveness. The tool Delain is 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.
Optimizing the Construction of the LTS CSD/BSD
Chloe's main function is to generate the LTSs CSD_b(N) and BSD_b(N) from given open net N and a bound b. The reachability graph of inner(N) is calculated by LoLA and used to compute the LTSs CSD_b(N) and BSD_b(N). DOT files are generated as output.
Chloe 3 is a complete rewrite of Chloe with a new algorithm and many additional optimizations. The new algorithm and the optimizations are described here:
- Johannes Dewender. An Optimized Implementation for a Trace-Based Characterization of b-Bounded Responsiveness. Diplomarbeit, Humboldt-Universität zu Berlin, 2015.
Chloe is open source software, licensed under the AGPL3+.
Installing and running Chloe requires a bunch of other tools:
- GCC - The GCC compiler
- 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.
- 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.
- Autotools test suite - Part of the GNU Auto-Tools for automated Tests
- 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 .
- 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.
- 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.
Extract the tar ball into a folder of your choice, and follow the steps below.
- Test (optional, but recommended)
sudo make install
Chloe's manual explains usage, features, and a brief scientifical background. If you are further interested learning more about the science behind Chloe, please consult Chloe's science section.
Chloe'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 Chloe is Johannes Dewender.
Johannes Dewender implemented the new algorithm and the optimizations.
Several people have committed time, code, and advice to the development of Chloe.
- Johannes Dewender (216 commits)
Chloe's development team thanks:
- Richard Müller for ideas, help and the theory
- Niels Lohmann for creating Wendy and writing several relevant papers
- Simon Heiden for creating the original Chloe