Learn more about Chloe
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.