Learn more about Delain

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.