Computer Systems Verification

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

Dynamic and Self-adaptive Architectures

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

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

Multi-paradigm modeling of sCPS a IoT

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

Performance Awareness in Software Development

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...

Processing and Visualizing IoT Data

As part of of our approaches to self-adaptation of distributed IoT and CPS systems, we focus also on processing the data coming from IoT and CPS systems. We developed a tool called IVIS, which This is needed 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

  • 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

Trust in Industry 4.0 Systems

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