Research Topics

Symbolic techniques and tools (such as SAT and SMT solvers and theorem provers) are used in program verification (establishing interesting properties, such as deadlock absence, race conditions, no assertion violation) to overcome the scaling issues of explicit-state approaches. Some of these methods employ Craig interpolants as an abstract way of representation sets of states. Our research focuses on extending this idea to further improve performance of the verification tools in terms of both verification time and consumed memory.   More...

Grants and Projects

• GAČR 23-06506S: Advanced Analysis and Verification for Advanced Software
• GAČR 20-07487S: Scalable Techniques for Analysis of Complex Properties of Computer Systems
• GAČR 17-12465S: Verification and Bug-Hunting for Advanced Software

As sCPS and IoT need to strike a balance between dependability, open-endedness and adaptability, and operate in dynamic and opportunistic environments, this makes their design design and development is challenging, especially when smartness in terms of ad-hoc cooperation and self-adaptation is pursued. Due to limited connectivity, sCPS typically have to perform coordination and adaptation in a decentralized manner, which further adds to the overall complexity of designing the adaptation. We focus on designing and developing self-adaptation and coordination techniques and methods suitable for sCPS and IoT. In particular, we employ the concept of autonomic component ensembles to describe cooperation and adaptation. This work has been started in the project ASCENS is further being extended.   More...

Results and Artifacts

• DEECo – A component model targeting design of systems consisting of autonomous, self-aware, and adaptable components (link)

Grants and Projects

• Autonomic Service Component Ensembles (ASCENS), FP7 IP project, 2011 – 2015
• Trans-European Research Training Network on Engineering and Provisioning of Service Based Cloud Applications (RELATE), FP7 Marie Curie Initial Training Network, 2011 – 2015

Edge cloud computing has been the recent trend to provide computation capacity to modern software-intensive IoT and smart CPS. These systems are built as highly distributed architectures of mobile and networked embedded devices. The edge-cloud computing allows these systems to incorporate cloud and while coping with issues related to latency and reliability, security and other non-functional properties. In our research, we specifically focus on the problem of providing probabilistic guarantees on response time of application running in the edge-cloud. We deal with this in the frame of upcoming projects AFarCloud and FITOPTIVIS.   More...

Grants and Projects

• From the cloud to the edge - smart IntegraTion and OPtimisation Technologies for highly efficient Image and VIdeo processing Systems (FitOptiVis), ECSEL, 2018 – 2020
• Aggregate Farming in the Cloud (AFarCloud), ECSEL, 2018 – 2020

We focus on state-of-the-art methods of model-driven development, requirements-oriented design, and component-based modeling and development. We focus on alignment of models from different fields, which allows us to combine at the architecture level models describing structure, coordination, communication (in mobile ad-hoc networks and infrastructure networks), physical laws, probability, etc. We have developed these models for multi-paradigm modeling of dynamic CPS via extended ensembles of autonomic components in the project MPM4CPS (COST). These results are further extended in the collaboration with our academic partners - GSSI (Italy), Chalmers University (Sweden).   More...

Results and Artifacts

• TCOOF – Trait-based Coalition Formation Framework. A framework for logical design of cooperating agents supporting composable multi-paradigm concerns. (link)

Grants and Projects

• Multi-Paradigm Modelling for Cyber-Physical Systems (COST IC 1404, supported by parallel national grant of Ministry of Education and Sports of the Czech Republic), 2015 – 2017

Software performance tends to be easier to observe after the fact than to design up front. Focusing on the implementation phases of software development, we work on methods that help improve developer awareness of software performance.   More...

As part of our approaches to the self-adaptation of distributed IoT and CPS systems, we also focus on processing the data coming from IoT and CPS systems. We have developed the IVIS platform for processing and visualizing IoT and CPS data. The platform provides a web-based interface that allows both the definition of complex visualizations and data processing jobs as well as exploring the data. Compared to the existing open-source and commercial offerings, IVIS follows a different model and focuses on flexibility. Instead of providing a complex administrative UI for creating visualizations by dragging and dropping components onto a dashboard, IVIS provides a set of JavaScript-based visualization components that are glued together using simple JavaScript code. Similarly, data processing jobs can be defined using code in scripting languages, such as Python, which allows for the exploitation of the wealth of existing libraries for numerical processing. This not only makes the definition of visualizations and data processing jobs much more expressive, but it also turns out to be significantly more straightforward to use when building complex parametric visualizations - especially when they need to deal with many sensors. This proved to be crucial in deploying IVIS in a number of international research projects because it enabled us to rapidly set up complex visualizations and data-processing tasks, catering to project- and partner-specific requirements.   More...

Results and Artifacts

• IVIS – A web-based framework for visualization of IoT data (link)

Grants and Projects

• Environmental Sensing To Act for a Better quality of Life: Smart Health (ESTABLISH), ITEA3/EUREKA project, 2017 – 2019
• From the cloud to the edge - smart IntegraTion and OPtimisation Technologies for highly efficient Image and VIdeo processing Systems (FitOptiVis), ECSEL, 2018 – 2020
• Aggregate Farming in the Cloud (AFarCloud), ECSEL, 2018 – 2020

Our tools shape how we think and what we can do. A new way of thinking about programming can make complex problems disappear, while a different programming paradigm or a novel implementation can enable new capabilities that were previously hard to imagine. We work on understanding, designing and implementing programming languages and systems that make programming simpler, more efficient, more accessible and trustworthy. We are interested in programming systems ranging from conventional programming languages to tools used by data scientists and end-user programming systems. We leverage a variety of methods, including programming langauge theory, empirical studies of programming tools, but also human-computer interaction and interdisciplinary approaches.   More...

Grants and Projects

• PRIMUS/24/SCI/021: Type Systems for Data-Centric Programming (link)
• ERC-CZ LL2325: Engineering of Data Analysis Pipelines (link)

Industry 4.0 features ad-hoc cooperation between machines, humans, and organizations in supply and production chains. This ad-hoc horizontal cooperation in Industry 4.0 systems is a disruptive step that makes current privacy and trust mechanisms unsuitable as they are built around rigid hierarchical infrastructures. We exploit autonomic component ensembles to describe situations in which the ad-hoc cooperation takes place and tie is to contextual rules for privacy and security. This work is being performed in the context of a bi-lateral (Czech-German) applied research project TRUST4.0.   More...

Results and Artifacts

• TCOOF for Security – A prototype adaptation of TCOOF framework to resolve access permissions (link)

Grants and Projects

• Trust 4.0: Dataflow-based Privacy and Trust Modelling and Analysis in Industry 4.0 Systems, bi-lateral projects between Czech Republic (TAČR DELTA) and Germany (BMBF), 2018 – 2019