Model-Checking Cyber-Physical Systems (MC2PS)

Cyber-physical systems (CPS) can be described as smart systems that encompass seamlessly integrated and closely
interacting computational (i.e., hardware and software) and physical
components. Cyber-physical systems (CPS) are currently of interest in academia,
industry, and government due to their potentially significant impact on
society, environment, and economy. Examples of application of CPS include
precision farming, intelligent transportation, environmental control, avionics,
smart grid, traffic control and safety, process control, telemedicine,
manufacturing, and smart city engineering.

Cyber-physical systems are rapidly becoming business and mission critical to the success of many organizations. As systems
continue to evolve and become more dependent on CPS they will rely less on
human decision-making and more on computational intelligence. The challenge
here is to design CPS that are dependable, reliable, safe, and secure. However,
since CPS involve a high degree of complexity and integrate various sources in
physical, sensing, networking, computational and actuation domains it is not
trivial to achieve this goal. Moreover, various types of failures can occur at
any time and at any place thereby reducing the system-wide robustness of CPSs.

In the past decades, formal methods have been successfully used for the precise analysis of a variety of software,
hardware and physical systems. The main principle behind formal analysis of a
system is to construct a computer based mathematical model of the given system
and formally verify whether this model meets the provided specifications and
the required behavior. The rigorous exercise of developing a mathematical model
for the given system and analyzing this model using mathematical reasoning
usually increases the chances for catching subtle but critical design errors
that are often ignored by traditional techniques like paper-and-pencil based
proofs, numerical methods or simulation.

Two of the most commonly used formal verification methods are model checking and theorem proving. In this project,
we aim to provide a generic model checking approach for formal specification
and verification of software and/or system development artifacts produced in CPSs.
These artifacts are usually diverse, covering cyber and physical elements,
including requirements statements, specifications, software/system models,
analysis results, and generated code. We will first analyze the existing
approaches for constraint checking in CPS. Subsequently, we will focus on
traceability modeling and impact analysis of existing CPS artefacts. Based on
the output of these activities we will provide a systematic approach for model
checking that will be applied for CPS in the life sciences domains.