Research Topics

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.

Results / Artifacts:

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

Projects / Grants:

  • 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

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

Results / Artifacts:

  • work in progress

Projects / Grants:

  • 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

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

Results / Artifacts:

  • IVIS – A web-based framework for visualization of IoT data.

Projects / Grants:

  • Environmental Sensing To Act for a Better quality of Life: Smart Health (ESTABLISH), ITEA3/EUREKA project, 2017 – 2019

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

Results / Artifacts:

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

Projects / Grants:

  • 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

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.

Results / Artifacts:

  • DEECo – A component model targeting design of systems consisting of autonomous, self-aware, and adaptable components
  • IRM – A method and corresponding model that allow for requirements engineering and design of sCPS with a focus on dependability aspects

Projects / Grants:

  • 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

Interpolation techniques in software 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 extendeding this idea to further improve performance of the verification tools in terms of both verification time and consumed memory.

Results / Artifacts:

  • Jančík P., Alt L., Fedyukovich G., Hyvärinen A. E. J., Kofroň J., Sharygina N.: PVAIR: Partial Variable Assignment InterpolatoR, In proceedings of FASE'16, Eindhoven, Netherlands. The final publication is available at link.springer.com., April 2016 (Link)

Projects / Grants:

  • GAČR 14-11384S: Automatic Formal Analysis and Verification of Programs with Complex Unbounded Data and Control Structures
  • GAČR 17-12465S: Verification and Bug-Hunting for Advanced Software