Name Description Contact Sources
DEECo component model Component model (stands for Dependable Emergent Ensembles of Components) targeting design of systems consisting of autonomous, self-aware, and adaptable components. Tomáš Bureš
Vladimír Matěna
Git repository (Java implementation)
Git repository (C implementation)
DiSL Aspect-oriented framework for Java bytecode instrumentation. Notable features include extensible pointcut model, efficient access to static and dynamic program context, and high degree of code coverage. Lubomír Bulej Subversion repository
HelenOS Portable research operating system based on microkernel multiserver design paradigms and built using fine-grained software components. HelenOS is flexible, modular, extensible, fault-tolerant and easy to understand.
Martin Děcký
Vojtěch Horký
Bazaar repository
IRM (Invariant Refinement Method) Method and corresponding model that allows for designing software-intensive Cyber-Physical Systems (siCPS) with a focus on dependability aspects. Tomáš Bureš
JPF-Partial State Matching JPF extension improving state matching and reducing reachable state space Pavel Jančík
Jan Kofroň
JPF-static Practical Verification Using Static Analysis and Java Pathfinder Pavel Parízek
JPMF Measurement Framework Java framework for collecting performance measurements. Provides a generic interface for defining performance event sources that emit performance events. Configuration then determines what events and metrics are collected and stored by the library, also paying attention to overhead. Lubomír Bulej Subversion repository
Panda Predicate Abstraction in Dynamic Analysis Jakub Daniel
Pavel Parízek
Git repository
Random Program Generator Framework for generating applications assembled randomly from available components. The purpose of the tool is to provide many implementations of software systems together with their performance models, to facilitate automated performance model validation. Petr Tůma Source archive
SPL Performance Documentation Tools Support for generating performance documentation in Java. Performance unit tests are used to measure documented performance, the generated documentation extends standard Javadoc. Vojtěch Horký
SPL Performance Testing Tools Support for unit testing of performance in Java. Performance assertions are specified as annotations, measurements of unit tests with performance assertions are provided in report form, assertion violations are reported. Vojtěch Horký
Petr Tůma
Git repository (core)
Git repository (Hudson plugin)
Git repository (Eclipse plugin)
Testbed for Experiments with Adaptation in Smart Cyber-Physical Systems Simulation platform based on Robotic Operating System(ROS), Stage robot simulator and OMNeT++ network simulator. Vladimír Matěna
Tomáš Bureš
(Main testbed repo)
(jDEECo implementation)
(Wireless board ROS integration)
(Wireless board firmware and Java interface)
(Remote simulation runner)
(OMNeT++ ROS integration)
WeVerca Static analysis framework for security analyses of PHP applications David Hauzar
Jan Kofroň
Git repository


Name Description Contact Sources


SOFA 2 component framework Component framework employing hierarchically composed components and providing features like ADL-based design, behavior specification using behavior protocols, automatically generated connectors supporting seamless and transparent distribution of applications, and distributed runtime environment with dynamic update of components. Petr Hnětynka Subversion repository


Gimple Model Checker Model checker of the Gimple intermediate code produced by the GCC compiler Jan Kofroň
Xampler Comprehensive CORBA benchmark suite, tests transport of all types and multiple scalability axes. Supports many brokers in C++ and Java, includes scripts for generating HTML report. Petr Tůma Git repository (benchmark)
Git repository (plotting utility)
Git repository (reporting scripts)


SOFA HI SOFA High Integrity is a profile of the SOFA 2 project targeting embedded, safety and mission-critical domains. Tomáš Bureš Subversion repository


COMBAT Component Behavior Analysis Toolset Pavel Parízek


Sampler Short CORBA benchmark suite, tests ping time and scalability with argument size, object count and thread count. Supports many brokers in C++ and Java, includes PHP website for browsing results. Petr Tůma Git repository


IDLtester Tool for testing OMG IDL compilers. Generates random IDL files of preset complexity together with code that uses the IDL compiler output. This helps check both parsing and code generation. Petr Tůma Source archive
IIOPtester Tool for testing OMG IIOP engines. Interposes a proxy between the server and the clients and applies configurable damage to IIOP messages during forwarding. This helps check IIOP engine robustness. Petr Tůma Source archive
Logo of Faculty of Mathematics and Physics
  • Phone: +420 951 554 267, +420 951 554 236
  • Email: info<at-sign>
  • How to find us?
Modified on 2016-04-04